118 |
118 |
119 val tfrees = fold Term.add_tfrees (prop :: As) []; |
119 val tfrees = fold Term.add_tfrees (prop :: As) []; |
120 val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees; |
120 val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees; |
121 |
121 |
122 val global_prop = |
122 val global_prop = |
123 Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop))); |
123 cert (Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop)))) |
|
124 |> Thm.weaken_sorts (Variable.sorts_of ctxt); |
124 val global_result = result |> Future.map |
125 val global_result = result |> Future.map |
125 (Thm.adjust_maxidx_thm ~1 #> |
126 (Thm.adjust_maxidx_thm ~1 #> |
126 Drule.implies_intr_list assms #> |
127 Drule.implies_intr_list assms #> |
127 Drule.forall_intr_list fixes #> |
128 Drule.forall_intr_list fixes #> |
128 Thm.generalize (map #1 tfrees, []) 0); |
129 Thm.generalize (map #1 tfrees, []) 0); |
129 val local_result = |
130 val local_result = |
130 Thm.future global_result (cert global_prop) |
131 Thm.future global_result global_prop |
131 |> Thm.instantiate (instT, []) |
132 |> Thm.instantiate (instT, []) |
132 |> Drule.forall_elim_list fixes |
133 |> Drule.forall_elim_list fixes |
133 |> fold (Thm.elim_implies o Thm.assume) assms; |
134 |> fold (Thm.elim_implies o Thm.assume) assms; |
134 in local_result end; |
135 in local_result end; |
135 |
136 |