92 fun reveal_bounds Ts = |
92 fun reveal_bounds Ts = |
93 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) |
93 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) |
94 (0 upto length Ts - 1 ~~ Ts)) |
94 (0 upto length Ts - 1 ~~ Ts)) |
95 |
95 |
96 (* Removes the lambdas from an equation of the form "t = (%x. u)". |
96 (* Removes the lambdas from an equation of the form "t = (%x. u)". |
97 (Cf. "extensionalize_theorem" in "Clausifier".) *) |
97 (Cf. "extensionalize_theorem" in "Meson_Clausifier".) *) |
98 fun extensionalize_term t = |
98 fun extensionalize_term t = |
99 let |
99 let |
100 fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t' |
100 fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t' |
101 | aux j (t as Const (s, Type (_, [Type (_, [_, T']), |
101 | aux j (t as Const (s, Type (_, [Type (_, [_, T']), |
102 Type (_, [_, res_T])])) |
102 Type (_, [_, res_T])])) |
139 t |
139 t |
140 else |
140 else |
141 t |> conceal_bounds Ts |
141 t |> conceal_bounds Ts |
142 |> Envir.eta_contract |
142 |> Envir.eta_contract |
143 |> cterm_of thy |
143 |> cterm_of thy |
144 |> Clausifier.introduce_combinators_in_cterm |
144 |> Meson_Clausifier.introduce_combinators_in_cterm |
145 |> prop_of |> Logic.dest_equals |> snd |
145 |> prop_of |> Logic.dest_equals |> snd |
146 |> reveal_bounds Ts |
146 |> reveal_bounds Ts |
147 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single |
147 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single |
148 in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end |
148 in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end |
149 handle THM _ => |
149 handle THM _ => |