Fix cmlPEGScript.sml

Author: dnezam

compiler/parsing/cmlPEGScript.sml

@@ -810,13 +810,12 @@ local
           SOME(e,t') => recurse (e :: acc) t'
         | NONE => acc
   val nts = recurse [] r
-in
-val FDOM_cmlPEG_nts = let
   fun p t = Q.prove(`^t ∈ FDOM cmlPEG.rules`, simp[FDOM_cmlPEG])
 in
 Theorem FDOM_cmlPEG_nts[simp] = LIST_CONJ (map p nts);
 end
-val NTS_in_PEG_exprs = let
+
+local
   val exprs_th' = REWRITE_RULE [pnt_def] PEG_exprs
                                            |> INST_TYPE [alpha |-> “:string”]
   val exprs_t = rhs (concl exprs_th')
@@ -838,5 +837,3 @@ val NTS_in_PEG_exprs = let
 in
 Theorem NTS_in_PEG_exprs[simp] = th;
 end
-
-end (* local *)