equal
deleted
inserted
replaced
45 let |
45 let |
46 val (args as {context, params, ...}, st') = focus ctxt i st; |
46 val (args as {context, params, ...}, st') = focus ctxt i st; |
47 fun export_closed th = |
47 fun export_closed th = |
48 let |
48 let |
49 val (th' :: params') = ProofContext.export context ctxt (th :: map Drule.mk_term params); |
49 val (th' :: params') = ProofContext.export context ctxt (th :: map Drule.mk_term params); |
50 val vs = map (#2 o Thm.dest_comb o Drule.strip_imp_concl o Thm.cprop_of) params'; |
50 val vs = map (Thm.dest_arg o Drule.strip_imp_concl o Thm.cprop_of) params'; |
51 in Drule.forall_intr_list vs th' end; |
51 in Drule.forall_intr_list vs th' end; |
52 fun retrofit th = Thm.compose_no_flatten false (th, 0) i; |
52 fun retrofit th = Thm.compose_no_flatten false (th, 0) i; |
53 in Seq.lifts retrofit (Seq.map (Goal.finish #> export_closed) (tac args st')) st end |
53 in Seq.lifts retrofit (Seq.map (Goal.finish #> export_closed) (tac args st')) st end |
54 |
54 |
55 end; |
55 end; |