src/HOL/Import/shuffler.ML
changeset 14818 ad83019a66a4
parent 14620 1be590fd2422
child 14848 83f1dc18f1f1
     1.1 --- a/src/HOL/Import/shuffler.ML	Sat May 29 14:55:56 2004 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Sat May 29 14:57:39 2004 +0200
     1.3 @@ -58,10 +58,8 @@
     1.4  (*Prints an exception, then fails*)
     1.5  fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
     1.6  
     1.7 -val string_of_thm = Library.setmp print_mode [] string_of_thm
     1.8 -val string_of_cterm = Library.setmp print_mode [] string_of_cterm
     1.9 -
    1.10 -val commafy = String.concat o separate ", "
    1.11 +val string_of_thm = Library.setmp print_mode [] (Output.output o string_of_thm);
    1.12 +val string_of_cterm = Library.setmp print_mode [] (Output.output o string_of_cterm);
    1.13  
    1.14  fun mk_meta_eq th =
    1.15      (case concl_of th of