src/HOL/Tools/Meson/meson_clausify.ML

 structure Meson_Clausify : MESON_CLAUSIFY =
 struct
 
 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****)
 
 val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
 val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);