equal
deleted
inserted
replaced
220 fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th); |
220 fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th); |
221 |
221 |
222 val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1; |
222 val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1; |
223 val rule = Thm.incr_indexes (maxidx + 1) raw_rule; |
223 val rule = Thm.incr_indexes (maxidx + 1) raw_rule; |
224 |
224 |
225 val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule)); |
225 val params = Rule_Cases.strip_params (Logic.nth_prem (1, Thm.prop_of rule)); |
226 val m = length vars; |
226 val m = length vars; |
227 val n = length params; |
227 val n = length params; |
228 val _ = m <= n orelse err "More variables than parameters in obtained rule" rule; |
228 val _ = m <= n orelse err "More variables than parameters in obtained rule" rule; |
229 |
229 |
230 fun unify ((x, T), (y, U)) (tyenv, max) = Sign.typ_unify thy (T, U) (tyenv, max) |
230 fun unify ((x, T), (y, U)) (tyenv, max) = Sign.typ_unify thy (T, U) (tyenv, max) |