--- a/src/Pure/Isar/method.ML Tue Jun 07 15:44:18 2016 +0200
+++ b/src/Pure/Isar/method.ML Tue Jun 07 19:55:45 2016 +0200
@@ -54,8 +54,9 @@
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 get_facts: Proof.context -> thm list
- val map_facts: (thm list -> thm list) -> Proof.context -> Proof.context
+ val update_facts: (thm list -> thm list) -> Proof.context -> Proof.context
type combinator_info
val no_combinator_info: combinator_info
datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int
@@ -376,12 +377,14 @@
(* method facts *)
+val clean_facts = filter_out Thm.is_dummy;
+
val get_facts_generic = these o #facts o Data.get;
val get_facts = get_facts_generic o Context.Proof;
-fun map_facts f =
+fun update_facts f =
(Context.proof_map o map_data)
- (fn (methods, ml_tactic, facts) => (methods, ml_tactic, SOME (f (these facts))));
+ (fn (methods, ml_tactic, facts) => (methods, ml_tactic, SOME (clean_facts (f (these facts)))));
val _ =
Theory.setup
@@ -570,7 +573,7 @@
| 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 (map_facts (K facts) ctxt, st)) end;
+ in fn facts => fn (ctxt, st) => method (Seq.Result (update_facts (K facts) ctxt, st)) end;
end;
--- a/src/Pure/Isar/proof.ML Tue Jun 07 15:44:18 2016 +0200
+++ b/src/Pure/Isar/proof.ML Tue Jun 07 19:55:45 2016 +0200
@@ -716,12 +716,9 @@
(* chain *)
-fun clean_facts ctxt =
- set_facts (filter_out Thm.is_dummy (the_facts ctxt)) ctxt;
-
val chain =
assert_forward
- #> clean_facts
+ #> (fn state => set_facts (Method.clean_facts (the_facts state)) state)
#> enter_chain;
fun chain_facts facts =