removed traces of former 'includes' element;
authorwenzelm
Thu Nov 20 00:03:55 2008 +0100 (2008-11-20)
changeset 28858855e61829e22
parent 28857 87d638a4ee67
child 28859 d50b523c55db
removed traces of former 'includes' element;
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/specification.ML	Thu Nov 20 00:03:53 2008 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Thu Nov 20 00:03:55 2008 +0100
     1.3 @@ -319,24 +319,16 @@
     1.4  );
     1.5  
     1.6  fun gen_theorem prep_att prep_stmt
     1.7 -    kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy0 =
     1.8 +    kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy =
     1.9    let
    1.10 -    val _ = LocalTheory.affirm lthy0;
    1.11 -    val thy = ProofContext.theory_of lthy0;
    1.12 -
    1.13 -    val (loc, ctxt, lthy) =
    1.14 -      (case (TheoryTarget.peek lthy0, false (* exists (fn Locale.Expr _ => true | _ => false) raw_elems *)) of
    1.15 -        ({target, is_locale = true, ...}, true) =>
    1.16 -          (*temporary workaround for non-modularity of in/includes*)  (* FIXME *)
    1.17 -          (SOME target, ProofContext.init thy, LocalTheory.restore lthy0)
    1.18 -      | _ => (NONE, lthy0, lthy0));
    1.19 +    val _ = LocalTheory.affirm lthy;
    1.20 +    val thy = ProofContext.theory_of lthy;
    1.21  
    1.22      val attrib = prep_att thy;
    1.23      val atts = map attrib raw_atts;
    1.24 -
    1.25      val elems = raw_elems |> map (Element.map_ctxt_attrib attrib);
    1.26      val ((prems, stmt, facts), goal_ctxt) =
    1.27 -      prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;
    1.28 +      prep_statement attrib (prep_stmt NONE) elems raw_concl lthy;
    1.29  
    1.30      fun after_qed' results goal_ctxt' =
    1.31        let val results' =