Skip to content

Commit 5d280ed

Browse files
committed
Fix cmlPEGScript.sml
1 parent be2374c commit 5d280ed

File tree

1 file changed

+2
-3
lines changed

1 file changed

+2
-3
lines changed

compiler/parsing/cmlPEGScript.sml

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -810,13 +810,12 @@ local
810810
SOME(e,t') => recurse (e :: acc) t'
811811
| NONE => acc
812812
val nts = recurse [] r
813-
in
814-
val FDOM_cmlPEG_nts = let
815813
fun p t = Q.prove(`^t ∈ FDOM cmlPEG.rules`, simp[FDOM_cmlPEG])
816814
in
817815
Theorem FDOM_cmlPEG_nts[simp] = LIST_CONJ (map p nts);
818816
end
819-
val NTS_in_PEG_exprs = let
817+
818+
local
820819
val exprs_th' = REWRITE_RULE [pnt_def] PEG_exprs
821820
|> INST_TYPE [alpha |-> “:string”]
822821
val exprs_t = rhs (concl exprs_th')

0 commit comments

Comments
 (0)