src/HOL/Import/proof_kernel.ML
changeset 17917 3c6e7760da89
parent 17894 f2fdd22accaa
child 17959 8db36a108213
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Oct 19 21:52:28 2005 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Oct 19 21:52:29 2005 +0200
     1.3 @@ -226,9 +226,10 @@
     1.4   
     1.5  val smart_string_of_thm = smart_string_of_cterm o cprop_of
     1.6  
     1.7 -fun prth th = writeln ((Library.setmp print_mode [] string_of_thm) th)
     1.8 -fun prc ct = writeln ((Library.setmp print_mode [] string_of_cterm) ct)
     1.9 -val prin = Library.setmp print_mode [] prin
    1.10 +fun prth th = writeln (Library.setmp print_mode [] string_of_thm th)
    1.11 +fun prc ct = writeln (Library.setmp print_mode [] string_of_cterm ct)
    1.12 +fun prin t = writeln
    1.13 +  (Library.setmp print_mode [] (fn () => Sign.string_of_term (the_context ()) t) ());
    1.14  fun pth (HOLThm(ren,thm)) =
    1.15      let
    1.16  	(*val _ = writeln "Renaming:"
    1.17 @@ -1939,8 +1940,6 @@
    1.18      end
    1.19      handle e => (message "exception in new_definition"; print_exn e)
    1.20  
    1.21 -val commafy = String.concat o separate ", "
    1.22 -
    1.23  local
    1.24      val helper = thm "termspec_help"
    1.25  in
    1.26 @@ -1952,7 +1951,7 @@
    1.27  	    val _ = message "NEW_SPEC:"
    1.28  	    val _ = if_debug pth hth
    1.29  	    val names = map (rename_const thyname thy) names
    1.30 -	    val _ = warning ("Introducing constants " ^ (commafy names))
    1.31 +	    val _ = warning ("Introducing constants " ^ commas names)
    1.32  	    val (HOLThm(rens,th)) = norm_hthm thy hth
    1.33  	    val thy1 = case HOL4DefThy.get thy of
    1.34  			   Replaying _ => thy
    1.35 @@ -2079,7 +2078,7 @@
    1.36  			| _ => error "Internal error in ProofKernel.new_typedefinition"
    1.37  	    val tnames_string = if null tnames
    1.38  				then ""
    1.39 -				else "(" ^ (commafy tnames) ^ ") "
    1.40 +				else "(" ^ commas tnames ^ ") "
    1.41  	    val proc_prop = if null tnames
    1.42  			    then smart_string_of_cterm
    1.43  			    else Library.setmp show_all_types true smart_string_of_cterm
    1.44 @@ -2173,7 +2172,7 @@
    1.45  	    
    1.46  	    val tnames_string = if null tnames
    1.47  				then ""
    1.48 -				else "(" ^ (commafy tnames) ^ ") "
    1.49 +				else "(" ^ commas tnames ^ ") "
    1.50  	    val proc_prop = if null tnames
    1.51  			    then smart_string_of_cterm
    1.52  			    else Library.setmp show_all_types true smart_string_of_cterm