--- a/src/Pure/Isar/proof.ML Sun Jul 29 14:30:05 2007 +0200
+++ b/src/Pure/Isar/proof.ML Sun Jul 29 14:30:06 2007 +0200
@@ -588,7 +588,7 @@
(* chain *)
fun clean_facts ctxt =
- put_facts (SOME (filter_out Drule.is_dummy_thm (the_facts ctxt))) ctxt;
+ put_facts (SOME (filter_out Thm.is_dummy (the_facts ctxt))) ctxt;
val chain =
assert_forward
@@ -651,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 @ filter_out Drule.is_dummy_thm ths;
+fun append_using _ ths using = using @ filter_out Thm.is_dummy ths;
fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt ths);
val unfold_goals = LocalDefs.unfold_goals;