# HG changeset patch
# User wenzelm
# Date 1185566121 -7200
# Node ID 8f2703c02241686b89b9e24cdbbc07d6d7a66d34
# Parent  2ef318813e1a89b3c702acb3fddddbe39332b5c7
chain/using: filter out dummy_thm;

diff -r 2ef318813e1a -r 8f2703c02241 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Jul 27 21:55:20 2007 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Jul 27 21:55:21 2007 +0200
@@ -587,9 +587,12 @@
 
 (* chain *)
 
+fun clean_facts ctxt =
+  put_facts (SOME (filter_out Drule.is_dummy_thm (the_facts ctxt))) ctxt;
+
 val chain =
   assert_forward
-  #> tap the_facts
+  #> clean_facts
   #> enter_chain;
 
 fun chain_facts facts =
@@ -648,7 +651,7 @@
         val ths = maps snd named_facts;
       in (statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end));
 
-fun append_using _ ths using = using @ ths;
+fun append_using _ ths using = using @ filter_out Drule.is_dummy_thm ths;
 fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt ths);
 val unfold_goals = LocalDefs.unfold_goals;