equal
deleted
inserted
replaced
164 |> try HOLogic.dest_Trueprop |
164 |> try HOLogic.dest_Trueprop |
165 in |
165 in |
166 case lhs_eq of |
166 case lhs_eq of |
167 SOME (Const (@{const_name HOL.eq}, _) $ _ $ _) => SOME (@{thm refl} RS thm) |
167 SOME (Const (@{const_name HOL.eq}, _) $ _ $ _) => SOME (@{thm refl} RS thm) |
168 | SOME _ => (case body_type (fastype_of lhs) of |
168 | SOME _ => (case body_type (fastype_of lhs) of |
169 Type (typ_name, _) => ( SOME |
169 Type (typ_name, _) => |
170 (#equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name)) |
170 try (fn () => |
171 RS @{thm Equiv_Relations.equivp_reflp} RS thm) |
171 #equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name)) |
172 handle _ => NONE) |
172 RS @{thm Equiv_Relations.equivp_reflp} RS thm) () |
173 | _ => NONE |
173 | _ => NONE |
174 ) |
174 ) |
175 | _ => NONE |
175 | _ => NONE |
176 end |
176 end |
177 |
177 |