tuned signature;

--- a/src/Pure/Isar/bundle.ML	Wed Mar 21 21:06:31 2012 +0100
+++ b/src/Pure/Isar/bundle.ML	Wed Mar 21 21:24:13 2012 +0100
@@ -103,9 +103,9 @@
 val includes = gen_includes (K I);
 val includes_cmd = gen_includes check;
 
-fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.put_facts NONE;
+fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts;
 fun include_cmd bs =
-  Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.put_facts NONE;
+  Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts;
 
 fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
 fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);

--- a/src/Pure/Isar/expression.ML	Wed Mar 21 21:06:31 2012 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Mar 21 21:24:13 2012 +0100
@@ -860,7 +860,7 @@
     fun after_qed witss eqns =
       (Proof.map_context o Context.proof_map)
         (note_eqns_register deps witss attrss eqns export export')
-      #> Proof.put_facts NONE;
+      #> Proof.reset_facts;
   in
     state
     |> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int

--- a/src/Pure/Isar/proof.ML	Wed Mar 21 21:06:31 2012 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Mar 21 21:24:13 2012 +0100
@@ -23,7 +23,8 @@
   val put_thms: bool -> string * thm list option -> state -> state
   val the_facts: state -> thm list
   val the_fact: state -> thm
-  val put_facts: thm list option -> state -> state
+  val set_facts: thm list -> state -> state
+  val reset_facts: state -> state
   val assert_forward: state -> state
   val assert_chain: state -> state
   val assert_forward_or_chain: state -> state
@@ -231,16 +232,19 @@
   map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
   put_thms true (Auto_Bind.thisN, facts);
 
+val set_facts = put_facts o SOME;
+val reset_facts = put_facts NONE;
+
 fun these_factss more_facts (named_factss, state) =
-  (named_factss, state |> put_facts (SOME (maps snd named_factss @ more_facts)));
+  (named_factss, state |> set_facts (maps snd named_factss @ more_facts));
 
 fun export_facts inner outer =
   (case get_facts inner of
-    NONE => put_facts NONE outer
+    NONE => reset_facts outer
   | SOME thms =>
       thms
       |> Proof_Context.export (context_of inner) (context_of outer)
-      |> (fn ths => put_facts (SOME ths) outer));
+      |> (fn ths => set_facts ths outer));
 
 
 (* mode *)
@@ -283,6 +287,9 @@
 
 fun put_goal goal = map_current (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
 
+val set_goal = put_goal o SOME;
+val reset_goal = put_goal NONE;
+
 val before_qed = #before_qed o #2 o current_goal;
 
 
@@ -298,7 +305,7 @@
       in map_context f (State (nd, node' :: nodes')) end
   | map_goal _ _ state = state;
 
-fun set_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) =>
+fun provide_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) =>
   (statement, [], using, goal, before_qed, after_qed));
 
 fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) =>
@@ -412,10 +419,10 @@
   |> ALLGOALS Goal.conjunction_tac
   |> Seq.maps (fn goal =>
     state
-    |> Seq.lift set_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1))
+    |> Seq.lift provide_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1))
     |> Seq.maps meth
     |> Seq.maps (fn state' => state'
-      |> Seq.lift set_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
+      |> Seq.lift provide_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
     |> Seq.maps (apply_method true (K Method.succeed)));
 
 fun apply_text cc text state =
@@ -471,7 +478,7 @@
   in
     raw_rules
     |> Proof_Context.goal_export inner outer
-    |> (fn rules => Seq.lift set_goal (EVERY (map refine rules) goal) state)
+    |> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
   end;
 
 end;
@@ -548,7 +555,7 @@
   state
   |> assert_forward
   |> map_context (bind true args #> snd)
-  |> put_facts NONE;
+  |> reset_facts;
 
 in
 
@@ -565,7 +572,7 @@
 fun gen_write prep_arg mode args =
   assert_forward
   #> map_context (fn ctxt => ctxt |> Proof_Context.notation true mode (map (prep_arg ctxt) args))
-  #> put_facts NONE;
+  #> reset_facts;
 
 in
 
@@ -585,7 +592,7 @@
 fun gen_fix prep_vars args =
   assert_forward
   #> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (prep_vars args ctxt)) ctxt))
-  #> put_facts NONE;
+  #> reset_facts;
 
 in
 
@@ -635,7 +642,7 @@
     |-> (fn vars =>
       map_context_result (prep_binds false (map swap raw_rhss))
       #-> (fn rhss => map_context_result (Local_Defs.add_defs (vars ~~ (name_atts ~~ rhss)))))
-    |-> (put_facts o SOME o map (#2 o #2))
+    |-> (set_facts o map (#2 o #2))
   end;
 
 in
@@ -652,7 +659,7 @@
 (* chain *)
 
 fun clean_facts ctxt =
-  put_facts (SOME (filter_out Thm.is_dummy (the_facts ctxt))) ctxt;
+  set_facts (filter_out Thm.is_dummy (the_facts ctxt)) ctxt;
 
 val chain =
   assert_forward
@@ -660,7 +667,7 @@
   #> enter_chain;
 
 fun chain_facts facts =
-  put_facts (SOME facts)
+  set_facts facts
   #> chain;
 
 
@@ -765,15 +772,15 @@
 val begin_block =
   assert_forward
   #> open_block
-  #> put_goal NONE
+  #> reset_goal
   #> open_block;
 
 val next_block =
   assert_forward
   #> close_block
   #> open_block
-  #> put_goal NONE
-  #> put_facts NONE;
+  #> reset_goal
+  #> reset_facts;
 
 fun end_block state =
   state
@@ -889,12 +896,12 @@
   in
     goal_state
     |> map_context (init_context #> Variable.set_body true)
-    |> put_goal (SOME (make_goal (statement, [], [], Goal.init goal, before_qed, after_qed')))
+    |> set_goal (make_goal (statement, [], [], Goal.init goal, before_qed, after_qed'))
     |> map_context (Proof_Context.auto_bind_goal props)
     |> chaining ? (`the_facts #-> using_facts)
-    |> put_facts NONE
+    |> reset_facts
     |> open_block
-    |> put_goal NONE
+    |> reset_goal
     |> enter_backward
     |> not (null vars) ? refine_terms (length goal_propss)
     |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)