# HG changeset patch
# User blanchet
# Date 1404898552 -7200
# Node ID 99a8e1cc7e9e49483cd611c2d077f0abca170943
# Parent  c7dc1f0a2b8ac82b25f963a08f55c4ce205ea0a5
get rid of some pointer equalities

diff -r c7dc1f0a2b8a -r 99a8e1cc7e9e src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 09 11:35:52 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 09 11:35:52 2014 +0200
@@ -1452,7 +1452,7 @@
              max_ary = max_ary, types = types, in_conj = in_conj}
           val fun_var_Ts' = fun_var_Ts |> can dest_funT T ? insert_type thy I T
         in
-          if bool_vars' = bool_vars andalso pointer_eq (fun_var_Ts', fun_var_Ts) then accum
+          if bool_vars' = bool_vars andalso fun_var_Ts' = fun_var_Ts then accum
           else ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab)
         end
       else
@@ -1477,7 +1477,7 @@
                    val min_ary =
                      if (app_op_level = Sufficient_App_Op orelse
                          app_op_level = Sufficient_App_Op_And_Predicator)
-                        andalso not (pointer_eq (types', types)) then
+                        andalso types' <> types then
                        fold (consider_var_ary T) fun_var_Ts min_ary
                      else
                        min_ary