# HG changeset patch
# User wenzelm
# Date 1227135835 -3600
# Node ID 855e61829e22e456a015bb0aff2d3fc4b46d1b58
# Parent  87d638a4ee6762eb6c708d4a43bc9685c3572bcb
removed traces of former 'includes' element;

diff -r 87d638a4ee67 -r 855e61829e22 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Nov 20 00:03:53 2008 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Nov 20 00:03:55 2008 +0100
@@ -319,24 +319,16 @@
 );
 
 fun gen_theorem prep_att prep_stmt
-    kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy0 =
+    kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy =
   let
-    val _ = LocalTheory.affirm lthy0;
-    val thy = ProofContext.theory_of lthy0;
-
-    val (loc, ctxt, lthy) =
-      (case (TheoryTarget.peek lthy0, false (* exists (fn Locale.Expr _ => true | _ => false) raw_elems *)) of
-        ({target, is_locale = true, ...}, true) =>
-          (*temporary workaround for non-modularity of in/includes*)  (* FIXME *)
-          (SOME target, ProofContext.init thy, LocalTheory.restore lthy0)
-      | _ => (NONE, lthy0, lthy0));
+    val _ = LocalTheory.affirm lthy;
+    val thy = ProofContext.theory_of lthy;
 
     val attrib = prep_att thy;
     val atts = map attrib raw_atts;
-
     val elems = raw_elems |> map (Element.map_ctxt_attrib attrib);
     val ((prems, stmt, facts), goal_ctxt) =
-      prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;
+      prep_statement attrib (prep_stmt NONE) elems raw_concl lthy;
 
     fun after_qed' results goal_ctxt' =
       let val results' =