renamed Drule.is_dummy_thm to Thm.is_dummy;
authorwenzelm
Sun Jul 29 14:30:06 2007 +0200 (2007-07-29)
changeset 24050248da5f0e735
parent 24049 e4adf8175149
child 24051 896fb015079c
renamed Drule.is_dummy_thm to Thm.is_dummy;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Sun Jul 29 14:30:05 2007 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Sun Jul 29 14:30:06 2007 +0200
     1.3 @@ -588,7 +588,7 @@
     1.4  (* chain *)
     1.5  
     1.6  fun clean_facts ctxt =
     1.7 -  put_facts (SOME (filter_out Drule.is_dummy_thm (the_facts ctxt))) ctxt;
     1.8 +  put_facts (SOME (filter_out Thm.is_dummy (the_facts ctxt))) ctxt;
     1.9  
    1.10  val chain =
    1.11    assert_forward
    1.12 @@ -651,7 +651,7 @@
    1.13          val ths = maps snd named_facts;
    1.14        in (statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end));
    1.15  
    1.16 -fun append_using _ ths using = using @ filter_out Drule.is_dummy_thm ths;
    1.17 +fun append_using _ ths using = using @ filter_out Thm.is_dummy ths;
    1.18  fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt ths);
    1.19  val unfold_goals = LocalDefs.unfold_goals;
    1.20