Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A more explicit prefix because gensym now generates easily predicatable
authorpaulson
Tue, 18 Mar 1997 15:15:01 +0100
changeset 2807 04c080e60f31
parent 2806 772f6bba48a1
child 2808 e8a224e41b9f
A more explicit prefix because gensym now generates easily predicatable identifiers
src/Pure/tctical.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle