60 val tsig = #tsig(Sign.rep_sg sg) |
60 val tsig = #tsig(Sign.rep_sg sg) |
61 val goali = nth_subgoal i state |
61 val goali = nth_subgoal i state |
62 val Ts = map #2 (Logic.strip_params goali) |
62 val Ts = map #2 (Logic.strip_params goali) |
63 val _ $ t $ _ = Logic.strip_assums_concl goali; |
63 val _ $ t $ _ = Logic.strip_assums_concl goali; |
64 val cntxt = mk_context cmap (rev Ts) (#maxidx(rep_thm lift)) t |
64 val cntxt = mk_context cmap (rev Ts) (#maxidx(rep_thm lift)) t |
65 val cu = Sign.cterm_of sg cntxt |
65 val cu = cterm_of sg cntxt |
66 val uT = #T(Sign.rep_cterm cu) |
66 val uT = #T(rep_cterm cu) |
67 val cP' = Sign.cterm_of sg (Var(P,uT)) |
67 val cP' = cterm_of sg (Var(P,uT)) |
68 val ixnTs = Type.typ_match tsig ([],(PT,uT)); |
68 val ixnTs = Type.typ_match tsig ([],(PT,uT)); |
69 val ixncTs = map (fn (x,y) => (x,Sign.ctyp_of sg y)) ixnTs; |
69 val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs; |
70 in instantiate (ixncTs, [(cP',cu)]) lift end; |
70 in instantiate (ixncTs, [(cP',cu)]) lift end; |
71 |
71 |
72 fun splittable al i thm = |
72 fun splittable al i thm = |
73 let val tm = goal_concl i thm |
73 let val tm = goal_concl i thm |
74 fun nobound j k (Abs(_,_,t)) = nobound j (k+1) t |
74 fun nobound j k (Abs(_,_,t)) = nobound j (k+1) t |