tuned comment
authorblanchet
Thu, 07 Apr 2011 12:16:25 +0200
changeset 42269 554e90f9db0c
parent 42261 611856e8cb1e
child 42270 5f2960582e45
tuned comment
src/HOL/Tools/Meson/meson_clausify.ML
--- 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)