avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
authorblanchet
Wed, 23 Mar 2011 10:18:42 +0100
changeset 429431492ee6b8085
parent 42942 04577a7e0c51
child 42944 217a1b61d42d
avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
src/HOL/Tools/Meson/meson_clausify.ML
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Wed Mar 23 10:06:27 2011 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Wed Mar 23 10:18:42 2011 +0100
     1.3 @@ -22,9 +22,9 @@
     1.4  
     1.5  open Meson
     1.6  
     1.7 -(* the extra "?" helps prevent clashes *)
     1.8 -val new_skolem_var_prefix = "?SK"
     1.9 -val new_nonskolem_var_prefix = "?V"
    1.10 +(* the extra "Meson" helps prevent clashes (FIXME) *)
    1.11 +val new_skolem_var_prefix = "MesonSK"
    1.12 +val new_nonskolem_var_prefix = "MesonV"
    1.13  
    1.14  (**** Transformation of Elimination Rules into First-Order Formulas****)
    1.15