src/Pure/Isar/locale.ML

     ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
     theory -> (theory * ProofContext.context) * (bstring * thm list) list
   val note_thmss_i: string -> string ->
     ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     theory -> (theory * ProofContext.context) * (bstring * thm list) list
-  val theorem: string -> (context * thm list -> thm list list -> theory -> theory) ->
+  val theorem: string -> Method.text option ->
+    (context * thm list -> thm list list -> theory -> theory) ->
     string * Attrib.src list -> element elem_expr list ->
     ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
     theory -> Proof.state
-  val theorem_i: string -> (context * thm list -> thm list list -> theory -> theory) ->
+  val theorem_i: string -> Method.text option ->
+    (context * thm list -> thm list list -> theory -> theory) ->
     string * theory attribute list -> element_i elem_expr list ->
     ((string * theory attribute list) * (term * (term list * term list)) list) list ->
     theory -> Proof.state
-  val theorem_in_locale: string ->
+  val theorem_in_locale: string -> Method.text option ->
     ((context * context) * thm list -> thm list list -> theory -> theory) ->
     xstring -> string * Attrib.src list -> element elem_expr list ->
     ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
     theory -> Proof.state
-  val theorem_in_locale_i: string ->
+  val theorem_in_locale_i: string -> Method.text option ->
     ((context * context) * thm list -> thm list list -> theory -> theory) ->
     string -> string * Attrib.src list -> element_i elem_expr list ->
     ((string * Attrib.src list) * (term * (term list * term list)) list) list ->
     theory -> Proof.state
   val smart_theorem: string -> xstring option ->

   | activate_elem _ ((ctxt, Assumed axs), Assumes asms) =
       let
         val asms' = Attrib.map_specs (Attrib.context_attribute_i ctxt) asms;
         val ts = List.concat (map (map #1 o #2) asms');
         val (ps, qs) = splitAt (length ts, axs);
-        val (ctxt', _) =
+        val (_, ctxt') =
           ctxt |> ProofContext.fix_frees ts
           |> ProofContext.assume_i (export_axioms ps) asms';
       in ((ctxt', Assumed qs), []) end
   | activate_elem _ ((ctxt, Derived ths), Assumes asms) =
       ((ctxt, Derived ths), [])
   | activate_elem _ ((ctxt, Assumed axs), Defines defs) =
       let
         val defs' = Attrib.map_specs (Attrib.context_attribute_i ctxt) defs;
-        val (ctxt', _) =
+        val (_, ctxt') =
         ctxt |> ProofContext.assume_i ProofContext.export_def
           (defs' |> map (fn ((name, atts), (t, ps)) =>
             let val (c, t') = ProofContext.cert_def ctxt t
             in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
       in ((ctxt', Assumed axs), []) end
   | activate_elem _ ((ctxt, Derived ths), Defines defs) =
       ((ctxt, Derived ths), [])
   | activate_elem is_ext ((ctxt, mode), Notes facts) =
       let
         val facts' = Attrib.map_facts (Attrib.context_attribute_i ctxt) facts;
-        val (ctxt', res) = ctxt |> ProofContext.note_thmss_i facts';
+        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i facts';
       in ((ctxt', mode), if is_ext then res else []) end;
 
 fun activate_elems (((name, ps), mode), elems) ctxt =
   let
     val ((ctxt', _), res) =

 (* parameters *)
 
 local
 
 fun prep_parms prep_vars ctxt parms =
-  let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T) => ([x], T)) parms))
+  let val vars = fst (fold_map prep_vars (map (fn (x, T) => ([x], T)) parms) ctxt)
   in map (fn ([x'], T') => (x', T')) vars end;
 
 in
 
 fun read_parms x = prep_parms ProofContext.read_vars x;

 
 fun local_note_accesses_i prfx args ctxt =
   ctxt
   |> ProofContext.qualified_names
   |> ProofContext.custom_accesses (local_accesses prfx)
-  |> ProofContext.note_thmss_i args
+  |> ProofContext.note_thmss_i args |> swap
   |>> ProofContext.restore_naming ctxt;
 
 end;
 
 

 local
 
 fun global_goal prep_att =
   Proof.global_goal ProofDisplay.present_results prep_att ProofContext.bind_propp_schematic_i;
 
-fun gen_theorem prep_att prep_elem prep_stmt kind after_qed a raw_elems concl thy =
+fun gen_theorem prep_att prep_elem prep_stmt kind before_qed after_qed a raw_elems concl thy =
   let
     val thy_ctxt = ProofContext.init thy;
     val elems = map (prep_elem thy) raw_elems;
     val (_, (_, view), _, ctxt, propp) = prep_stmt NONE elems (map snd concl) thy_ctxt;
     val ctxt' = ctxt |> ProofContext.add_view thy_ctxt view;
     val stmt = map fst concl ~~ propp;
-  in global_goal prep_att kind after_qed (SOME "") a stmt ctxt' end;
+  in global_goal prep_att kind before_qed after_qed (SOME "") a stmt ctxt' end;
 
 fun gen_theorem_in_locale prep_locale prep_src prep_elem prep_stmt no_target
-    kind after_qed raw_locale (name, atts) raw_elems concl thy =
+    kind before_qed after_qed raw_locale (name, atts) raw_elems concl thy =
   let
     val locale = prep_locale thy raw_locale;
     val locale_atts = map (prep_src thy) atts;
     val locale_attss = map (map (prep_src thy) o snd o fst) concl;
     val target = if no_target then NONE else SOME (extern thy locale);

           if name = "" andalso null locale_atts then I
           else #2 o add_thmss kind locale [((name, locale_atts), List.concat (map #2 res'))])
         #> #2
         #> after_qed ((goal_ctxt, locale_ctxt'), raw_results) results
       end;
-  in global_goal (K I) kind after_qed' target (name, []) stmt elems_ctxt'' end;
+  in global_goal (K I) kind before_qed after_qed' target (name, []) stmt elems_ctxt'' end;
 
 in
 
 val theorem = gen_theorem Attrib.global_attribute intern_attrib_elem_expr read_context_statement;
 val theorem_i = gen_theorem (K I) (K I) cert_context_statement;

 val theorem_in_locale_i = gen_theorem_in_locale (K I) (K I) (K I) cert_context_statement false;
 val theorem_in_locale_no_target =
   gen_theorem_in_locale (K I) (K I) (K I) cert_context_statement true;
 
 fun smart_theorem kind NONE a [] concl =
-      Proof.theorem kind (K (K I)) (SOME "") a concl o ProofContext.init
+      Proof.theorem kind NONE (K (K I)) (SOME "") a concl o ProofContext.init
   | smart_theorem kind NONE a elems concl =
-      theorem kind (K (K I)) a elems concl
+      theorem kind NONE (K (K I)) a elems concl
   | smart_theorem kind (SOME loc) a elems concl =
-      theorem_in_locale kind (K (K I)) loc a elems concl;
+      theorem_in_locale kind NONE (K (K I)) loc a elems concl;
 
 end;
 
 
 (** Interpretation commands **)

     val thy_ctxt = ProofContext.init thy;
     val (propss, activate) = prep_global_registration (prfx, atts) expr insts thy;
     val kind = goal_name thy "interpretation" NONE propss;
     fun after_qed (goal_ctxt, raw_results) _ =
       activate (map (ProofContext.export_plain goal_ctxt thy_ctxt) raw_results);
-  in Proof.theorem_i kind after_qed NONE ("", []) (prep_propp propss) thy_ctxt end;
+  in Proof.theorem_i kind NONE after_qed NONE ("", []) (prep_propp propss) thy_ctxt end;
 
 fun interpretation_in_locale (raw_target, expr) thy =
   let
     val target = intern thy raw_target;
     val (propss, activate) = prep_registration_in_locale target expr thy;
     val kind = goal_name thy "interpretation" (SOME target) propss;
     fun after_qed ((goal_ctxt, locale_ctxt), raw_results) _ =
       activate (map (ProofContext.export_plain goal_ctxt locale_ctxt) raw_results);
-  in theorem_in_locale_no_target kind after_qed target ("", []) [] (prep_propp propss) thy end;
+  in theorem_in_locale_no_target kind NONE after_qed target ("", []) [] (prep_propp propss) thy end;
 
 fun interpret (prfx, atts) expr insts int state =
   let
     val ctxt = Proof.context_of state;
     val (propss, activate) = prep_local_registration (prfx, atts) expr insts ctxt;

       Proof.map_context (K (ctxt |> activate raw_results))
       #> Proof.put_facts NONE
       #> Seq.single;
   in
     Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
-      kind after_qed (prep_propp propss) state
+      kind NONE after_qed (prep_propp propss) state
   end;
 
 end;
 
 end;