# HG changeset patch
# User blanchet
# Date 1302171385 -7200
# Node ID 554e90f9db0ca37732a6c53ee602f7acbd0213e0
# Parent  611856e8cb1e8130a09d528f17bf1ec1350eadb4
tuned comment

diff -r 611856e8cb1e -r 554e90f9db0c 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)