# HG changeset patch
# User blanchet
# Date 1300871922 -3600
# Node ID 1492ee6b8085b7e7169e0cae0904b2332b429b2f
# Parent  04577a7e0c51fea48864f94a0363d0352c81fca0
avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"

diff -r 04577a7e0c51 -r 1492ee6b8085 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Wed Mar 23 10:06:27 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Wed Mar 23 10:18:42 2011 +0100
@@ -22,9 +22,9 @@
 
 open Meson
 
-(* the extra "?" helps prevent clashes *)
-val new_skolem_var_prefix = "?SK"
-val new_nonskolem_var_prefix = "?V"
+(* the extra "Meson" helps prevent clashes (FIXME) *)
+val new_skolem_var_prefix = "MesonSK"
+val new_nonskolem_var_prefix = "MesonV"
 
 (**** Transformation of Elimination Rules into First-Order Formulas****)