oops -- no Output.out here;
authorwenzelm
Mon May 31 08:53:23 2004 +0200 (2004-05-31)
changeset 1484883f1dc18f1f1
parent 14847 44d92c12b255
child 14849 73a0a6e0426a
oops -- no Output.out here;
src/HOL/Import/import_package.ML
src/HOL/Import/shuffler.ML
     1.1 --- a/src/HOL/Import/import_package.ML	Sat May 29 16:50:53 2004 +0200
     1.2 +++ b/src/HOL/Import/import_package.ML	Mon May 31 08:53:23 2004 +0200
     1.3 @@ -30,8 +30,8 @@
     1.4  val debug = ref false
     1.5  fun message s = if !debug then writeln s else ()
     1.6  
     1.7 -val string_of_thm = Library.setmp print_mode [] (Output.output o string_of_thm);
     1.8 -val string_of_cterm = Library.setmp print_mode [] (Output.output o string_of_cterm);
     1.9 +val string_of_thm = Library.setmp print_mode [] string_of_thm;
    1.10 +val string_of_cterm = Library.setmp print_mode [] string_of_cterm;
    1.11  
    1.12  fun import_tac (thyname,thmname) =
    1.13      if !SkipProof.quick_and_dirty
     2.1 --- a/src/HOL/Import/shuffler.ML	Sat May 29 16:50:53 2004 +0200
     2.2 +++ b/src/HOL/Import/shuffler.ML	Mon May 31 08:53:23 2004 +0200
     2.3 @@ -58,8 +58,8 @@
     2.4  (*Prints an exception, then fails*)
     2.5  fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
     2.6  
     2.7 -val string_of_thm = Library.setmp print_mode [] (Output.output o string_of_thm);
     2.8 -val string_of_cterm = Library.setmp print_mode [] (Output.output o string_of_cterm);
     2.9 +val string_of_thm = Library.setmp print_mode [] string_of_thm;
    2.10 +val string_of_cterm = Library.setmp print_mode [] string_of_cterm;
    2.11  
    2.12  fun mk_meta_eq th =
    2.13      (case concl_of th of