equal
deleted
inserted
replaced
343 | (Bound i, Bound i') => |
343 | (Bound i, Bound i') => |
344 if i = i' then rtrm |
344 if i = i' then rtrm |
345 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
345 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
346 |
346 |
347 | (rt, qt) => |
347 | (rt, qt) => |
348 raise (LIFT_MATCH "regularize failed (default)") |
348 let val (rts, qts) = (Syntax.string_of_term lthy rt, Syntax.string_of_term lthy qt) in |
|
349 raise (LIFT_MATCH ("regularize failed (default: " ^ rts ^ "," ^ qts ^ ")")) |
|
350 end |
349 *} |
351 *} |
350 |
352 |
351 section {* Regularize Tactic *} |
353 section {* Regularize Tactic *} |
352 |
354 |
353 ML {* |
355 ML {* |