# HG changeset patch
# User wenzelm
# Date 1414787711 -3600
# Node ID 621c052789b42344ccb6b9db5ce7ec2d469a0f82
# Parent  897f266c44b301cf656474705fabdcdd3fd8ca05
obsolete;

diff -r 897f266c44b3 -r 621c052789b4 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Oct 31 21:20:06 2014 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Oct 31 21:35:11 2014 +0100
@@ -22,7 +22,6 @@
   val use_thys: (string * Position.T) list -> unit
   val use_thy: string * Position.T -> unit
   val script_thy: Position.T -> string -> theory
-  val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory
   val register_thy: theory -> unit
   val finish: unit -> unit
 end;
@@ -378,15 +377,6 @@
     val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
   in Toplevel.end_theory end_pos end_state end;
 
-fun toplevel_begin_theory master_dir (header: Thy_Header.header) =
-  let
-    val {name = (name, _), imports, ...} = header;
-    val _ = kill_thy name;
-    val _ = use_theories {document = false, last_timing = K NONE, master_dir = master_dir} imports;
-    val _ = Thy_Header.define_keywords header;
-    val parents = map (get_theory o base_name o fst) imports;
-  in Resources.begin_theory master_dir header parents end;
-
 
 (* register theory *)
 
diff -r 897f266c44b3 -r 621c052789b4 src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Fri Oct 31 21:20:06 2014 +0100
+++ b/src/Pure/pure_syn.ML	Fri Oct 31 21:35:11 2014 +0100
@@ -10,8 +10,8 @@
 val _ =
   Outer_Syntax.command
     (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
-    (Thy_Header.args >> (fn header =>
-      Toplevel.init_theory (fn () => Thy_Info.toplevel_begin_theory Path.current header)));
+    (Thy_Header.args >>
+      (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
 
 val _ =
   Outer_Syntax.command