# HG changeset patch
# User wenzelm
# Date 1129751549 -7200
# Node ID 3c6e7760da896a7cf045791f101d2f46f49621a2
# Parent  51269a053504f00fc13115a62d12743068175045
replaced commafy by existing commas;
avoid obsolete Goals.prin;

diff -r 51269a053504 -r 3c6e7760da89 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Wed Oct 19 21:52:28 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Wed Oct 19 21:52:29 2005 +0200
@@ -226,9 +226,10 @@
  
 val smart_string_of_thm = smart_string_of_cterm o cprop_of
 
-fun prth th = writeln ((Library.setmp print_mode [] string_of_thm) th)
-fun prc ct = writeln ((Library.setmp print_mode [] string_of_cterm) ct)
-val prin = Library.setmp print_mode [] prin
+fun prth th = writeln (Library.setmp print_mode [] string_of_thm th)
+fun prc ct = writeln (Library.setmp print_mode [] string_of_cterm ct)
+fun prin t = writeln
+  (Library.setmp print_mode [] (fn () => Sign.string_of_term (the_context ()) t) ());
 fun pth (HOLThm(ren,thm)) =
     let
 	(*val _ = writeln "Renaming:"
@@ -1939,8 +1940,6 @@
     end
     handle e => (message "exception in new_definition"; print_exn e)
 
-val commafy = String.concat o separate ", "
-
 local
     val helper = thm "termspec_help"
 in
@@ -1952,7 +1951,7 @@
 	    val _ = message "NEW_SPEC:"
 	    val _ = if_debug pth hth
 	    val names = map (rename_const thyname thy) names
-	    val _ = warning ("Introducing constants " ^ (commafy names))
+	    val _ = warning ("Introducing constants " ^ commas names)
 	    val (HOLThm(rens,th)) = norm_hthm thy hth
 	    val thy1 = case HOL4DefThy.get thy of
 			   Replaying _ => thy
@@ -2079,7 +2078,7 @@
 			| _ => error "Internal error in ProofKernel.new_typedefinition"
 	    val tnames_string = if null tnames
 				then ""
-				else "(" ^ (commafy tnames) ^ ") "
+				else "(" ^ commas tnames ^ ") "
 	    val proc_prop = if null tnames
 			    then smart_string_of_cterm
 			    else Library.setmp show_all_types true smart_string_of_cterm
@@ -2173,7 +2172,7 @@
 	    
 	    val tnames_string = if null tnames
 				then ""
-				else "(" ^ (commafy tnames) ^ ") "
+				else "(" ^ commas tnames ^ ") "
 	    val proc_prop = if null tnames
 			    then smart_string_of_cterm
 			    else Library.setmp show_all_types true smart_string_of_cterm