author | blanchet |
Thu, 07 Apr 2011 12:16:25 +0200 | |
changeset 42269 | 554e90f9db0c |
parent 42261 | 611856e8cb1e |
child 42270 | 5f2960582e45 |
--- a/src/HOL/Tools/Meson/meson_clausify.ML Wed Apr 06 18:36:28 2011 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Apr 07 12:16:25 2011 +0200 @@ -343,7 +343,7 @@ val fixes = Term.add_free_names (prop_of zapped_th) [] |> filter is_zapped_var_name - val ctxt' = ctxt |> Variable.add_fixes_direct fixes (*###*) + val ctxt' = ctxt |> Variable.add_fixes_direct fixes val fully_skolemized_t = zapped_th |> singleton (Variable.export ctxt' ctxt)