src/Pure/Isar/element.ML
changeset 19866 d47f32a4964a
parent 19843 67cb97e856ff
child 19897 fe661eb3b0e7
     1.1 --- a/src/Pure/Isar/element.ML	Mon Jun 12 21:19:05 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Mon Jun 12 21:19:06 2006 +0200
     1.3 @@ -310,7 +310,7 @@
     1.4  
     1.5  fun hyps_rule rule th =
     1.6    let
     1.7 -    val cterm_rule = Thm.reflexive #> rule #> Thm.cprop_of #> Drule.dest_equals #> #1;
     1.8 +    val cterm_rule = Drule.mk_term #> rule #> Drule.dest_term;
     1.9      val {hyps, ...} = Thm.crep_thm th;
    1.10    in
    1.11      Drule.implies_elim_list