src/HOL/Decision_Procs/ferrante_rackoff.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 40314 b5ec88d9ac03
     1.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -175,7 +175,7 @@
     1.4   let
     1.5    fun h bounds tm =
     1.6     (case term_of tm of
     1.7 -     Const (@{const_name "op ="}, T) $ _ $ _ =>
     1.8 +     Const (@{const_name HOL.eq}, T) $ _ $ _ =>
     1.9         if domain_type T = HOLogic.boolT then find_args bounds tm
    1.10         else Thm.dest_fun2 tm
    1.11     | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)