equal
deleted
inserted
replaced
172 kbo_advisory_simp_ordering (ord_info ()) |
172 kbo_advisory_simp_ordering (ord_info ()) |
173 else |
173 else |
174 Metis_KnuthBendixOrder.default |
174 Metis_KnuthBendixOrder.default |
175 fun fall_back () = |
175 fun fall_back () = |
176 (verbose_warning ctxt |
176 (verbose_warning ctxt |
177 ("Falling back on " ^ |
177 ("Falling back on " ^ quote (metis_call (hd fallback_type_encs) lam_trans) ^ "..."); |
178 quote (metis_call (hd fallback_type_encs) lam_trans) ^ "..."); |
|
179 FOL_SOLVE fallback_type_encs lam_trans ctxt cls ths0) |
178 FOL_SOLVE fallback_type_encs lam_trans ctxt cls ths0) |
180 in |
179 in |
181 (case filter (fn t => prop_of t aconv @{prop False}) cls of |
180 (case filter (fn t => prop_of t aconv @{prop False}) cls of |
182 false_th :: _ => [false_th RS @{thm FalseE}] |
181 false_th :: _ => [false_th RS @{thm FalseE}] |
183 | [] => |
182 | [] => |