src/Pure/Isar/specification.ML
changeset 28710 e2064974c114
parent 28703 aef727ef30e5
child 28791 cc16be808796
     1.1 --- a/src/Pure/Isar/specification.ML	Wed Oct 29 15:32:58 2008 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Thu Oct 30 10:57:45 2008 +0100
     1.3 @@ -47,11 +47,11 @@
     1.4      local_theory -> (string * thm list) list * local_theory
     1.5    val theorem: string -> Method.text option ->
     1.6      (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
     1.7 -    Element.context_i Locale.element list -> Element.statement_i ->
     1.8 +    Element.context_i list -> Element.statement_i ->
     1.9      bool -> local_theory -> Proof.state
    1.10    val theorem_cmd: string -> Method.text option ->
    1.11      (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
    1.12 -    Element.context Locale.element list -> Element.statement ->
    1.13 +    Element.context list -> Element.statement ->
    1.14      bool -> local_theory -> Proof.state
    1.15    val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
    1.16  end;
    1.17 @@ -273,8 +273,8 @@
    1.18            let val name = Name.name_of binding
    1.19            in if name = "" then string_of_int (i + 1) else name end);
    1.20          val constraints = obtains |> map (fn (_, (vars, _)) =>
    1.21 -          Locale.Elem (Element.Constrains
    1.22 -            (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE))));
    1.23 +          Element.Constrains
    1.24 +            (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE)));
    1.25  
    1.26          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
    1.27          val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt;
    1.28 @@ -325,7 +325,7 @@
    1.29      val thy = ProofContext.theory_of lthy0;
    1.30  
    1.31      val (loc, ctxt, lthy) =
    1.32 -      (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
    1.33 +      (case (TheoryTarget.peek lthy0, false (* exists (fn Locale.Expr _ => true | _ => false) raw_elems *)) of
    1.34          ({target, is_locale = true, ...}, true) =>
    1.35            (*temporary workaround for non-modularity of in/includes*)  (* FIXME *)
    1.36            (SOME target, ProofContext.init thy, LocalTheory.restore lthy0)
    1.37 @@ -334,7 +334,7 @@
    1.38      val attrib = prep_att thy;
    1.39      val atts = map attrib raw_atts;
    1.40  
    1.41 -    val elems = raw_elems |> map (Locale.map_elem (Element.map_ctxt_attrib attrib));
    1.42 +    val elems = raw_elems |> map (Element.map_ctxt_attrib attrib);
    1.43      val ((prems, stmt, facts), goal_ctxt) =
    1.44        prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;
    1.45