equal
deleted
inserted
replaced
108 |
108 |
109 |
109 |
110 (*** instantiation of adm_subst theorem (a bit tricky) ***) |
110 (*** instantiation of adm_subst theorem (a bit tricky) ***) |
111 |
111 |
112 fun inst_adm_subst_thm state i params s T subt t paths = |
112 fun inst_adm_subst_thm state i params s T subt t paths = |
113 let val {thy = sign, maxidx, ...} = rep_thm state; |
113 let |
114 val j = maxidx+1; |
114 val sign = Thm.theory_of_thm state; |
|
115 val j = Thm.maxidx_of state + 1; |
115 val parTs = map snd (rev params); |
116 val parTs = map snd (rev params); |
116 val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst}; |
117 val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst}; |
117 val types = valOf o (fst (types_sorts rule)); |
118 val types = valOf o (fst (types_sorts rule)); |
118 val tT = types ("t", j); |
119 val tT = types ("t", j); |
119 val PT = types ("P", j); |
120 val PT = types ("P", j); |