# HG changeset patch
# User paulson
# Date 1155141702 -7200
# Node ID dcb321249aa9815252b314bdbf4e8cb7052d6d16
# Parent  e42674e0486ea8d582310992f652af40739976db
consistent prefixing for skolem functions

diff -r e42674e0486e -r dcb321249aa9 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Wed Aug 09 18:39:08 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Wed Aug 09 18:41:42 2006 +0200
@@ -241,7 +241,7 @@
 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   It returns a modified theory, unless skolemization fails.*)
 fun skolem thy (name,th) =
-  let val cname = (case name of "" => gensym "sko" | s => Sign.base_name s)
+  let val cname = (case name of "" => gensym "sko_" | s => Sign.base_name s)
   in Option.map 
         (fn nnfth => 
           let val (thy',defs) = declare_skofuns cname nnfth thy