src/Pure/pure_thy.ML

--- a/src/Pure/pure_thy.ML	Fri Nov 09 00:18:23 2001 +0100
+++ b/src/Pure/pure_thy.ML	Fri Nov 09 00:19:20 2001 +0100
@@ -83,6 +83,7 @@
 
   val empty = mk_empty ();
   fun copy (ref x) = ref x;
+  val finish = I;
   val prep_ext = mk_empty;
   val merge = mk_empty;
 
@@ -386,6 +387,7 @@
 
   val empty = {name = "", version = 0};
   val copy = I;
+  val finish = I;
   val prep_ext  = I;
   fun merge _ = empty;
   fun print _ _ = ();
@@ -417,7 +419,10 @@
   |> put_name name
   |> local_path;
 
-fun end_theory thy = Theory.add_name (get_name thy) thy;
+fun end_theory thy =
+  thy
+  |> Theory.finish
+  |> Theory.add_name (get_name thy);
 
 fun checkpoint thy =
   if is_draft thy then
@@ -473,7 +478,6 @@
     ("itself", [logicS], logicS)]
   |> Theory.add_nonterminals Syntax.pure_nonterms
   |> Theory.add_syntax Syntax.pure_syntax
-  |> Theory.add_modesyntax (Symbol.symbolsN, true) Syntax.pure_sym_syntax
   |> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax
   |> Theory.add_trfuns Syntax.pure_trfuns
   |> Theory.add_trfunsT Syntax.pure_trfunsT