--- a/src/Pure/theory.ML Wed Aug 01 18:57:17 2012 +0200
+++ b/src/Pure/theory.ML Wed Aug 01 19:53:20 2012 +0200
@@ -138,16 +138,19 @@
fun at_end f = map_wrappers (apsnd (cons (f, stamp ())));
fun begin_theory name imports =
- let
- val thy = Context.begin_thy Context.pretty_global name imports;
- val wrappers = begin_wrappers thy;
- in
- thy
- |> Sign.local_path
- |> Sign.map_naming (Name_Space.set_theory_name name)
- |> apply_wrappers wrappers
- |> tap (Syntax.force_syntax o Sign.syn_of)
- end;
+ if name = Context.PureN then
+ (case imports of [thy] => thy | _ => error "Bad bootstrapping of theory Pure")
+ else
+ let
+ val thy = Context.begin_thy Context.pretty_global name imports;
+ val wrappers = begin_wrappers thy;
+ in
+ thy
+ |> Sign.local_path
+ |> Sign.map_naming (Name_Space.set_theory_name name)
+ |> apply_wrappers wrappers
+ |> tap (Syntax.force_syntax o Sign.syn_of)
+ end;
fun end_theory thy =
thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy;