--- 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
--- 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 =>
--- 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