src/HOL/Tools/meson.ML

   | nclauses _ = 1; (* literal *)
 
 (*Replaces universally quantified variables by FREE variables -- because
   assumptions may not contain scheme variables.  Later, call "generalize". *)
 fun freeze_spec th =
-  let val newname = gensym "A_"
+  let val newname = gensym "mes_"
       val spec' = read_instantiate [("x", newname)] spec
   in  th RS spec'  end;
 
 (*Used with METAHYPS below. There is one assumption, which gets bound to prem
   and then normalized via function nf. The normal form is given to resolve_tac,