src/HOL/Import/shuffler.ML
changeset 38864 4abe644fcea5
parent 38715 6513ea67d95d
child 39159 0dec18004e75
     1.1 --- a/src/HOL/Import/shuffler.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Import/shuffler.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -60,14 +60,14 @@
     1.4  
     1.5  fun mk_meta_eq th =
     1.6      (case concl_of th of
     1.7 -         Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th RS eq_reflection
     1.8 +         Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th RS eq_reflection
     1.9         | Const("==",_) $ _ $ _ => th
    1.10         | _ => raise THM("Not an equality",0,[th]))
    1.11      handle _ => raise THM("Couldn't make meta equality",0,[th])  (* FIXME avoid handle _ *)
    1.12  
    1.13  fun mk_obj_eq th =
    1.14      (case concl_of th of
    1.15 -         Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th
    1.16 +         Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th
    1.17         | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
    1.18         | _ => raise THM("Not an equality",0,[th]))
    1.19      handle _ => raise THM("Couldn't make object equality",0,[th])  (* FIXME avoid handle _ *)