Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed Drule.is_dummy_thm to Thm.is_dummy;
authorwenzelm
Sun, 29 Jul 2007 14:30:06 +0200
changeset 24050 248da5f0e735
parent 24049 e4adf8175149
child 24051 896fb015079c
renamed Drule.is_dummy_thm to Thm.is_dummy;
src/Pure/Isar/proof.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle