--- a/src/Pure/pure_syn.ML Thu Apr 16 14:18:32 2015 +0200
+++ b/src/Pure/pure_syn.ML Thu Apr 16 15:00:03 2015 +0200
@@ -4,7 +4,12 @@
Outer syntax for bootstrapping Isabelle/Pure.
*)
-structure Pure_Syn: sig end =
+signature PURE_SYN =
+sig
+ val bootstrap_thy: theory
+end;
+
+structure Pure_Syn: PURE_SYN =
struct
val _ =
@@ -44,5 +49,9 @@
(Thy_Header.args >>
(fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
+
+val bootstrap_thy = ML_Context.the_global_context ();
+
+val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false);
+
end;
-