src/HOL/Decision_Procs/langford.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 44121 44adaa6db327
     1.1 --- a/src/HOL/Decision_Procs/langford.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Decision_Procs/langford.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -116,7 +116,7 @@
     1.4  fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
     1.5  
     1.6  fun is_eqx x eq = case term_of eq of
     1.7 -   Const(@{const_name "op ="},_)$l$r => l aconv term_of x orelse r aconv term_of x
     1.8 +   Const(@{const_name HOL.eq},_)$l$r => l aconv term_of x orelse r aconv term_of x
     1.9   | _ => false ;
    1.10  
    1.11  local 
    1.12 @@ -176,7 +176,7 @@
    1.13   let
    1.14    fun h bounds tm =
    1.15     (case term_of tm of
    1.16 -     Const (@{const_name "op ="}, T) $ _ $ _ =>
    1.17 +     Const (@{const_name HOL.eq}, T) $ _ $ _ =>
    1.18         if domain_type T = HOLogic.boolT then find_args bounds tm
    1.19         else Thm.dest_fun2 tm
    1.20     | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)