144 in (Logic.list_all (params, t), (rev vs, subst_bounds (vs, t))) end; |
144 in (Logic.list_all (params, t), (rev vs, subst_bounds (vs, t))) end; |
145 |
145 |
146 fun inst_params thy (vs, p) th cts = |
146 fun inst_params thy (vs, p) th cts = |
147 let val env = Pattern.first_order_match thy (p, Thm.prop_of th) |
147 let val env = Pattern.first_order_match thy (p, Thm.prop_of th) |
148 (Vartab.empty, Vartab.empty) |
148 (Vartab.empty, Vartab.empty) |
149 in Thm.instantiate ([], |
149 in Thm.instantiate ([], map (dest_Var o Envir.subst_term env) vs ~~ cts) th end; |
150 map (Envir.subst_term env #> Thm.global_cterm_of thy) vs ~~ cts) th |
|
151 end; |
|
152 |
150 |
153 fun prove_strong_ind s alt_name avoids ctxt = |
151 fun prove_strong_ind s alt_name avoids ctxt = |
154 let |
152 let |
155 val thy = Proof_Context.theory_of ctxt; |
153 val thy = Proof_Context.theory_of ctxt; |
156 val ({names, ...}, {raw_induct, intrs, elims, ...}) = |
154 val ({names, ...}, {raw_induct, intrs, elims, ...}) = |