changeset 59848 | 18c21d5c9138 |
parent 59630 | c9aa1c90796f |
child 60217 | 40c63ffce97f |
--- 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