src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39192 f302ed18f42f
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -411,7 +411,7 @@
     1.4  fun conjuncts t = conjuncts_aux t [];
     1.5  
     1.6  fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
     1.7 -  | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
     1.8 +  | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
     1.9    | is_equationlike_term _ = false
    1.10    
    1.11  val is_equationlike = is_equationlike_term o prop_of