fixup! Fix cmlPEGScript.sml

Author: dnezam

compiler/parsing/cmlPEGScript.sml

@@ -810,31 +810,32 @@ local
           SOME(e,t') => recurse (e :: acc) t'
         | NONE => acc
   val nts = recurse [] r
-  fun p t = Q.prove(`^t ∈ FDOM cmlPEG.rules`, simp[FDOM_cmlPEG])
-  val th = LIST_CONJ (map p nts)
 in
-Theorem FDOM_cmlPEG_nts[simp] = th;
-end
 
-local
-  val exprs_th' = REWRITE_RULE [pnt_def] PEG_exprs
-                                           |> INST_TYPE [alpha |-> “:string”]
-  val exprs_t = rhs (concl exprs_th')
-  val nt = mk_thy_const{Thy = "peg", Name = "nt",
-                        Ty = ``:MMLnonT inf -> (mlptree list -> mlptree list) ->
-                                (token,MMLnonT,mlptree list,string) pegsym``}
-  val I_t = mk_thy_const{Thy = "combin", Name = "I",
-                         Ty = ``:mlptree list -> mlptree list``}
-  fun p t = let
-    val _ = print ("PEGexpr: "^term_to_string t^"\n")
-    val th0 = prove(pred_setSyntax.mk_in(list_mk_comb(nt,[t,I_t]), exprs_t),
-                    simp[pnt_def])
-              handle e => (print("Failed on "^term_to_string t^"\n");
-                           raise e)
+  local
+    fun p t = Q.prove(`^t ∈ FDOM cmlPEG.rules`, simp[FDOM_cmlPEG])
   in
-    CONV_RULE (RAND_CONV (K (SYM exprs_th'))) th0
+Theorem FDOM_cmlPEG_nts[simp] = LIST_CONJ (map p nts);
   end
-  val th = LIST_CONJ (map p nts)
-in
-Theorem NTS_in_PEG_exprs[simp] = th;
-end
+
+  local
+    val exprs_th' = REWRITE_RULE [pnt_def] PEG_exprs
+                                 |> INST_TYPE [alpha |-> “:string”]
+    val exprs_t = rhs (concl exprs_th')
+    val nt = mk_thy_const{Thy = "peg", Name = "nt",
+                          Ty = ``:MMLnonT inf -> (mlptree list -> mlptree list) ->
+                               (token,MMLnonT,mlptree list,string) pegsym``}
+    val I_t = mk_thy_const{Thy = "combin", Name = "I",
+                           Ty = ``:mlptree list -> mlptree list``}
+    fun p t = let
+      val _ = print ("PEGexpr: "^term_to_string t^"\n")
+      val th0 = prove(pred_setSyntax.mk_in(list_mk_comb(nt,[t,I_t]), exprs_t),
+                      simp[pnt_def])
+                handle e => (print("Failed on "^term_to_string t^"\n");
+                             raise e)
+    in CONV_RULE (RAND_CONV (K (SYM exprs_th'))) th0 end
+  in
+Theorem NTS_in_PEG_exprs[simp] = LIST_CONJ (map p nts);
+  end
+
+end (* local *)