# HG changeset patch
# User wenzelm
# Date 1465322145 -7200
# Node ID 9a20078425b1ec774d26eca16e685b92b5bf3495
# Parent  96cfb07c60d4c4bbb445815391a2a7f5d74ac356
clean facts more uniformly;

diff -r 96cfb07c60d4 -r 9a20078425b1 src/Pure/Isar/method.ML
--- 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;
 
diff -r 96cfb07c60d4 -r 9a20078425b1 src/Pure/Isar/proof.ML
--- 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 =