src/Pure/Isar/method.ML

   val erule: Proof.context -> int -> thm list -> method
   val drule: Proof.context -> int -> thm list -> method
   val frule: Proof.context -> int -> thm list -> method
   val set_tactic: (morphism -> thm list -> tactic) -> Context.generic -> Context.generic
   val clean_facts: thm list -> thm list
+  val set_facts: thm list -> Proof.context -> Proof.context
+  val get_facts: Proof.context -> thm list
   type combinator_info
   val no_combinator_info: combinator_info
   datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int
   datatype text =
     Source of Token.src |

 
 (* method facts *)
 
 val clean_facts = filter_out Thm.is_dummy;
 
+fun set_facts facts =
+  (Context.proof_map o map_data)
+    (fn (methods, ml_tactic, _) => (methods, ml_tactic, SOME (clean_facts facts)));
+
 val get_facts_generic = these o #facts o Data.get;
 val get_facts = get_facts_generic o Context.Proof;
-
-fun update_facts f =
-  (Context.proof_map o map_data)
-    (fn (methods, ml_tactic, facts) => (methods, ml_tactic, SOME (clean_facts (f (these facts)))));
 
 val _ =
   Theory.setup
     (Global_Theory.add_thms_dynamic (Binding.make ("method_facts", @{here}), get_facts_generic));
 

       Seq.single #> Seq.maps_results (fn (ctxt, st) => m (get_facts ctxt) (ctxt, st));
     fun eval (Basic m) = eval0 (m static_ctxt)
       | eval (Source src) = eval0 (method_cmd static_ctxt src static_ctxt)
       | eval (Combinator (_, c, txts)) = combinator c (map eval txts);
     val method = eval text;
-  in fn facts => fn (ctxt, st) => method (Seq.Result (update_facts (K facts) ctxt, st)) end;
+  in fn facts => fn (ctxt, st) => method (Seq.Result (set_facts facts ctxt, st)) end;
 
 end;