# 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