# HG changeset patch
# User paulson
# Date 858694501 -3600
# Node ID 04c080e60f31dd8c25e32b272de581ab638108a4
# Parent  772f6bba48a1379cb1339ddebd8f615ab91fc670
A more explicit prefix because gensym now generates easily predicatable
identifiers

diff -r 772f6bba48a1 -r 04c080e60f31 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Tue Mar 18 15:12:53 1997 +0100
+++ b/src/Pure/tctical.ML	Tue Mar 18 15:15:01 1997 +0100
@@ -347,7 +347,7 @@
   It is paired with a function to undo the transformation.  If ct contains
   Vars then it returns ct==>ct.*)
 fun eq_trivial ct =
-  let val xfree = cterm_of Sign.proto_pure (Free (gensym"X", propT))
+  let val xfree = cterm_of Sign.proto_pure (Free (gensym"EQ_TRIVIAL_", propT))
       val ct_eq_x = mk_prop_equals (ct, xfree)
       and refl_ct = reflexive ct
       fun restore th =