src/Pure/Isar/element.ML

--- a/src/Pure/Isar/element.ML	Sat Jul 31 21:14:20 2010 +0200
+++ b/src/Pure/Isar/element.ML	Sat Jul 31 21:14:20 2010 +0200
@@ -40,6 +40,9 @@
     term list list -> term list -> Proof.context -> Proof.state
   val witness_local_proof: (witness list list -> Proof.state -> Proof.state) ->
     string -> term list list -> Proof.context -> bool -> Proof.state -> Proof.state
+  val witness_local_proof_eqs: (witness list list -> thm list -> Proof.state -> Proof.state) ->
+    string -> term list list -> term list -> Proof.context -> bool -> Proof.state ->
+    Proof.state
   val morph_witness: morphism -> witness -> witness
   val conclude_witness: witness -> thm
   val pretty_witness: Proof.context -> witness -> Pretty.T
@@ -57,6 +60,8 @@
     (Attrib.binding * (thm list * Attrib.src list) list) list
   val eq_morphism: theory -> thm list -> morphism option
   val transfer_morphism: theory -> morphism
+  val generic_note_thmss: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
+    Context.generic -> (string * thm list) list * Context.generic
   val init: context_i -> Context.generic -> Context.generic
   val activate_i: context_i -> Proof.context -> context_i * Proof.context
   val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
@@ -280,6 +285,10 @@
       in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
   in proof after_qed' propss #> refine_witness #> Seq.hd end;
 
+fun proof_local cmd goal_ctxt int after_qed' propss =
+    Proof.map_context (K goal_ctxt)
+    #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
+      cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
 in
 
 fun witness_proof after_qed wit_propss =
@@ -289,12 +298,11 @@
 val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE);
 
 fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
-  gen_witness_proof (fn after_qed' => fn propss =>
-    Proof.map_context (K goal_ctxt)
-    #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
-      cmd NONE after_qed' (map (pair Thm.empty_binding) propss))
+  gen_witness_proof (proof_local cmd goal_ctxt int)
     (fn wits => fn _ => after_qed wits) wit_propss [];
 
+fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt int =
+  gen_witness_proof (proof_local cmd goal_ctxt int) after_qed wit_propss eq_props;
 end;
 
 
@@ -467,6 +475,15 @@
 
 (* init *)
 
+fun generic_note_thmss kind facts context =
+  let
+    val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
+  in
+    context |> Context.mapping_result
+      (PureThy.note_thmss kind facts')
+      (ProofContext.note_thmss kind facts')
+  end;
+
 fun init (Fixes fixes) = Context.map_proof (ProofContext.add_fixes fixes #> #2)
   | init (Constrains _) = I
   | init (Assumes asms) = Context.map_proof (fn ctxt =>
@@ -486,13 +503,7 @@
           |> fold Variable.auto_fixes (map #1 asms)
           |> ProofContext.add_assms_i Local_Defs.def_export (map #2 asms);
       in ctxt' end)
-  | init (Notes (kind, facts)) = (fn context =>
-      let
-        val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
-        val context' = context |> Context.mapping
-          (PureThy.note_thmss kind facts' #> #2)
-          (ProofContext.note_thmss kind facts' #> #2);
-      in context' end);
+  | init (Notes (kind, facts)) = generic_note_thmss kind facts #> #2;
 
 
 (* activate *)