# HG changeset patch
# User wenzelm
# Date 1427663283 -7200
# Node ID 18c21d5c913886a279ce150da847c87abbc39d74
# Parent  c5c4a936357acdb45e2dbe5891a06af5c4e8e948
clarified equality of formal entities;

diff -r c5c4a936357a -r 18c21d5c9138 src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Sun Mar 29 22:38:18 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Sun Mar 29 23:08:03 2015 +0200
@@ -128,7 +128,7 @@
        Pretty.str "found."]))
   end
 
-fun is_id_quot thm = (Thm.prop_of thm = Thm.prop_of @{thm identity_quotient})  (* FIXME equality!? *)
+fun is_id_quot thm = Thm.eq_thm_prop (thm, @{thm identity_quotient})
 
 fun zip_Tvars ctxt type_name rty_Tvars qty_Tvars =
   case try (get_rel_quot_thm ctxt) type_name of
diff -r c5c4a936357a -r 18c21d5c9138 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sun Mar 29 22:38:18 2015 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sun Mar 29 23:08:03 2015 +0200
@@ -531,12 +531,12 @@
       val tab = fold Termtab.update
         (map (fn eq =>
                 let val (s,t) = Thm.cprop_of eq |> Thm.dest_arg |> Thm.dest_binop
-                    val th = if Thm.term_of s = Thm.term_of t  (* FIXME equality? *)
-                             then the (Termtab.lookup inStab (Thm.term_of s))
-                             else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)
-                                [eq, the (Termtab.lookup inStab (Thm.term_of s))]
-                 in (Thm.term_of t, th) end)
-                  sths) Termtab.empty
+                    val th =
+                      if s aconvc t
+                      then the (Termtab.lookup inStab (Thm.term_of s))
+                      else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)
+                        [eq, the (Termtab.lookup inStab (Thm.term_of s))]
+                 in (Thm.term_of t, th) end) sths) Termtab.empty
         in
           fn ct => the (Termtab.lookup tab (Thm.term_of ct))
             handle Option.Option =>
diff -r c5c4a936357a -r 18c21d5c9138 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Sun Mar 29 22:38:18 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sun Mar 29 23:08:03 2015 +0200
@@ -355,7 +355,7 @@
     | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")"))
   end
 
-fun is_id_quot thm = (Thm.prop_of thm = Thm.prop_of @{thm identity_quotient3})  (* FIXME equality *)
+fun is_id_quot thm = Thm.eq_thm_prop (thm, @{thm identity_quotient3})
 
 open Lifting_Util