78 |> the_default @{term True} |
78 |> the_default @{term True} |
79 |> Ctr_Sugar_Util.list_exists_free vars |
79 |> Ctr_Sugar_Util.list_exists_free vars |
80 |> Term.map_abs_vars (Variable.revert_fixed ctxt) |
80 |> Term.map_abs_vars (Variable.revert_fixed ctxt) |
81 |> fold_rev Term.absfree (names ~~ Ts) |
81 |> fold_rev Term.absfree (names ~~ Ts) |
82 |> Thm.cterm_of ctxt; |
82 |> Thm.cterm_of ctxt; |
83 val thm = Ctr_Sugar_Util.cterm_instantiate_pos [SOME phi] raw_thm; |
83 val thm = infer_instantiate' ctxt [SOME phi] raw_thm; |
84 val e = length eqs; |
84 val e = length eqs; |
85 val p = length prems; |
85 val p = length prems; |
86 in |
86 in |
87 HEADGOAL (EVERY' [resolve_tac ctxt [thm], |
87 HEADGOAL (EVERY' [resolve_tac ctxt [thm], |
88 EVERY' (map (fn var => |
88 EVERY' (map (fn var => |
89 resolve_tac ctxt |
89 resolve_tac ctxt |
90 [Ctr_Sugar_Util.cterm_instantiate_pos |
90 [infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt var)] exI]) vars), |
91 [NONE, SOME (Thm.cterm_of ctxt var)] exI]) vars), |
|
92 if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs |
91 if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs |
93 else |
92 else |
94 REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN' |
93 REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN' |
95 Ctr_Sugar_Util.CONJ_WRAP' (resolve_tac ctxt o single) prems, |
94 Ctr_Sugar_Util.CONJ_WRAP' (resolve_tac ctxt o single) prems, |
96 K (ALLGOALS_SKIP skip |
95 K (ALLGOALS_SKIP skip |