src/HOL/simpdata.ML
changeset 20872 528054ca23e3
parent 20217 25b068a99d2b
child 20932 e65e1234c9d3
     1.1 --- a/src/HOL/simpdata.ML	Fri Oct 06 15:39:29 2006 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Sat Oct 07 01:30:58 2006 +0200
     1.3 @@ -272,7 +272,7 @@
     1.4    (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
     1.5       rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
     1.6     in mk_meta_eq rl' handle THM _ =>
     1.7 -     if Logic.is_equals (concl_of rl') then rl'
     1.8 +     if can Logic.dest_equals (concl_of rl') then rl'
     1.9       else error "Conclusion of congruence rules must be =-equality"
    1.10     end);
    1.11