src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 38864 4abe644fcea5
parent 38797 abe92b33ac9f
child 38957 2eb265efa1b0
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -587,7 +587,7 @@
     1.4  
     1.5  fun preprocess_elim ctxt elimrule =
     1.6    let
     1.7 -    fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
     1.8 +    fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, T) $ lhs $ rhs)) =
     1.9         HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
    1.10       | replace_eqs t = t
    1.11      val thy = ProofContext.theory_of ctxt