src/HOL/Tools/TFL/usyntax.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 43324 2b47822868e4
     1.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -244,7 +244,7 @@
     1.4       end
     1.5    | dest_abs _ _ =  raise USYN_ERR "dest_abs" "not an abstraction";
     1.6  
     1.7 -fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
     1.8 +fun dest_eq(Const(@{const_name HOL.eq},_) $ M $ N) = {lhs=M, rhs=N}
     1.9    | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
    1.10  
    1.11  fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}