1.1 --- a/src/Pure/Isar/locale.ML	Sat Oct 15 00:08:04 2005 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Sat Oct 15 00:08:05 2005 +0200
     1.3 @@ -91,20 +91,22 @@
     1.4    val note_thmss_i: string -> string ->
     1.5      ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     1.6      theory -> (theory * ProofContext.context) * (bstring * thm list) list
     1.7 -  val theorem: string -> (context * thm list -> thm list list -> theory -> theory) ->
     1.8 +  val theorem: string -> Method.text option ->
     1.9 +    (context * thm list -> thm list list -> theory -> theory) ->
    1.10      string * Attrib.src list -> element elem_expr list ->
    1.11      ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    1.12      theory -> Proof.state
    1.13 -  val theorem_i: string -> (context * thm list -> thm list list -> theory -> theory) ->
    1.14 +  val theorem_i: string -> Method.text option ->
    1.15 +    (context * thm list -> thm list list -> theory -> theory) ->
    1.16      string * theory attribute list -> element_i elem_expr list ->
    1.17      ((string * theory attribute list) * (term * (term list * term list)) list) list ->
    1.18      theory -> Proof.state
    1.19 -  val theorem_in_locale: string ->
    1.20 +  val theorem_in_locale: string -> Method.text option ->
    1.21      ((context * context) * thm list -> thm list list -> theory -> theory) ->
    1.22      xstring -> string * Attrib.src list -> element elem_expr list ->
    1.23      ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    1.24      theory -> Proof.state
    1.25 -  val theorem_in_locale_i: string ->
    1.26 +  val theorem_in_locale_i: string -> Method.text option ->
    1.27      ((context * context) * thm list -> thm list list -> theory -> theory) ->
    1.28      string -> string * Attrib.src list -> element_i elem_expr list ->
    1.29      ((string * Attrib.src list) * (term * (term list * term list)) list) list ->
    1.30 @@ -1087,7 +1089,7 @@
    1.31          val asms' = Attrib.map_specs (Attrib.context_attribute_i ctxt) asms;
    1.32          val ts = List.concat (map (map #1 o #2) asms');
    1.33          val (ps, qs) = splitAt (length ts, axs);
    1.34 -        val (ctxt', _) =
    1.35 +        val (_, ctxt') =
    1.36            ctxt |> ProofContext.fix_frees ts
    1.37            |> ProofContext.assume_i (export_axioms ps) asms';
    1.38        in ((ctxt', Assumed qs), []) end
    1.39 @@ -1096,7 +1098,7 @@
    1.40    | activate_elem _ ((ctxt, Assumed axs), Defines defs) =
    1.41        let
    1.42          val defs' = Attrib.map_specs (Attrib.context_attribute_i ctxt) defs;
    1.43 -        val (ctxt', _) =
    1.44 +        val (_, ctxt') =
    1.45          ctxt |> ProofContext.assume_i ProofContext.export_def
    1.46            (defs' |> map (fn ((name, atts), (t, ps)) =>
    1.47              let val (c, t') = ProofContext.cert_def ctxt t
    1.48 @@ -1107,7 +1109,7 @@
    1.49    | activate_elem is_ext ((ctxt, mode), Notes facts) =
    1.50        let
    1.51          val facts' = Attrib.map_facts (Attrib.context_attribute_i ctxt) facts;
    1.52 -        val (ctxt', res) = ctxt |> ProofContext.note_thmss_i facts';
    1.53 +        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i facts';
    1.54        in ((ctxt', mode), if is_ext then res else []) end;
    1.55  
    1.56  fun activate_elems (((name, ps), mode), elems) ctxt =
    1.57 @@ -1196,7 +1198,7 @@
    1.58  local
    1.59  
    1.60  fun prep_parms prep_vars ctxt parms =
    1.61 -  let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T) => ([x], T)) parms))
    1.62 +  let val vars = fst (fold_map prep_vars (map (fn (x, T) => ([x], T)) parms) ctxt)
    1.63    in map (fn ([x'], T') => (x', T')) vars end;
    1.64  
    1.65  in
    1.66 @@ -1732,7 +1734,7 @@
    1.67    ctxt
    1.68    |> ProofContext.qualified_names
    1.69    |> ProofContext.custom_accesses (local_accesses prfx)
    1.70 -  |> ProofContext.note_thmss_i args
    1.71 +  |> ProofContext.note_thmss_i args |> swap
    1.72    |>> ProofContext.restore_naming ctxt;
    1.73  
    1.74  end;
    1.75 @@ -2052,17 +2054,17 @@
    1.76  fun global_goal prep_att =
    1.77    Proof.global_goal ProofDisplay.present_results prep_att ProofContext.bind_propp_schematic_i;
    1.78  
    1.79 -fun gen_theorem prep_att prep_elem prep_stmt kind after_qed a raw_elems concl thy =
    1.80 +fun gen_theorem prep_att prep_elem prep_stmt kind before_qed after_qed a raw_elems concl thy =
    1.81    let
    1.82      val thy_ctxt = ProofContext.init thy;
    1.83      val elems = map (prep_elem thy) raw_elems;
    1.84      val (_, (_, view), _, ctxt, propp) = prep_stmt NONE elems (map snd concl) thy_ctxt;
    1.85      val ctxt' = ctxt |> ProofContext.add_view thy_ctxt view;
    1.86      val stmt = map fst concl ~~ propp;
    1.87 -  in global_goal prep_att kind after_qed (SOME "") a stmt ctxt' end;
    1.88 +  in global_goal prep_att kind before_qed after_qed (SOME "") a stmt ctxt' end;
    1.89  
    1.90  fun gen_theorem_in_locale prep_locale prep_src prep_elem prep_stmt no_target
    1.91 -    kind after_qed raw_locale (name, atts) raw_elems concl thy =
    1.92 +    kind before_qed after_qed raw_locale (name, atts) raw_elems concl thy =
    1.93    let
    1.94      val locale = prep_locale thy raw_locale;
    1.95      val locale_atts = map (prep_src thy) atts;
    1.96 @@ -2090,7 +2092,7 @@
    1.97          #> #2
    1.98          #> after_qed ((goal_ctxt, locale_ctxt'), raw_results) results
    1.99        end;
   1.100 -  in global_goal (K I) kind after_qed' target (name, []) stmt elems_ctxt'' end;
   1.101 +  in global_goal (K I) kind before_qed after_qed' target (name, []) stmt elems_ctxt'' end;
   1.102  
   1.103  in
   1.104  
   1.105 @@ -2103,11 +2105,11 @@
   1.106    gen_theorem_in_locale (K I) (K I) (K I) cert_context_statement true;
   1.107  
   1.108  fun smart_theorem kind NONE a [] concl =
   1.109 -      Proof.theorem kind (K (K I)) (SOME "") a concl o ProofContext.init
   1.110 +      Proof.theorem kind NONE (K (K I)) (SOME "") a concl o ProofContext.init
   1.111    | smart_theorem kind NONE a elems concl =
   1.112 -      theorem kind (K (K I)) a elems concl
   1.113 +      theorem kind NONE (K (K I)) a elems concl
   1.114    | smart_theorem kind (SOME loc) a elems concl =
   1.115 -      theorem_in_locale kind (K (K I)) loc a elems concl;
   1.116 +      theorem_in_locale kind NONE (K (K I)) loc a elems concl;
   1.117  
   1.118  end;
   1.119  
   1.120 @@ -2422,7 +2424,7 @@
   1.121      val kind = goal_name thy "interpretation" NONE propss;
   1.122      fun after_qed (goal_ctxt, raw_results) _ =
   1.123        activate (map (ProofContext.export_plain goal_ctxt thy_ctxt) raw_results);
   1.124 -  in Proof.theorem_i kind after_qed NONE ("", []) (prep_propp propss) thy_ctxt end;
   1.125 +  in Proof.theorem_i kind NONE after_qed NONE ("", []) (prep_propp propss) thy_ctxt end;
   1.126  
   1.127  fun interpretation_in_locale (raw_target, expr) thy =
   1.128    let
   1.129 @@ -2431,7 +2433,7 @@
   1.130      val kind = goal_name thy "interpretation" (SOME target) propss;
   1.131      fun after_qed ((goal_ctxt, locale_ctxt), raw_results) _ =
   1.132        activate (map (ProofContext.export_plain goal_ctxt locale_ctxt) raw_results);
   1.133 -  in theorem_in_locale_no_target kind after_qed target ("", []) [] (prep_propp propss) thy end;
   1.134 +  in theorem_in_locale_no_target kind NONE after_qed target ("", []) [] (prep_propp propss) thy end;
   1.135  
   1.136  fun interpret (prfx, atts) expr insts int state =
   1.137    let
   1.138 @@ -2444,7 +2446,7 @@
   1.139        #> Seq.single;
   1.140    in
   1.141      Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
   1.142 -      kind after_qed (prep_propp propss) state
   1.143 +      kind NONE after_qed (prep_propp propss) state
   1.144    end;
   1.145  
   1.146  end;