Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
oops -- no Output.out here;
authorwenzelm
Mon, 31 May 2004 08:53:23 +0200
changeset 14848 83f1dc18f1f1
parent 14847 44d92c12b255
child 14849 73a0a6e0426a
oops -- no Output.out here;
src/HOL/Import/import_package.ML file | annotate | diff | comparison | revisions
src/HOL/Import/shuffler.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Import/import_package.ML	Sat May 29 16:50:53 2004 +0200
+++ b/src/HOL/Import/import_package.ML	Mon May 31 08:53:23 2004 +0200
@@ -30,8 +30,8 @@
 val debug = ref false
 fun message s = if !debug then writeln s else ()
 
-val string_of_thm = Library.setmp print_mode [] (Output.output o string_of_thm);
-val string_of_cterm = Library.setmp print_mode [] (Output.output o string_of_cterm);
+val string_of_thm = Library.setmp print_mode [] string_of_thm;
+val string_of_cterm = Library.setmp print_mode [] string_of_cterm;
 
 fun import_tac (thyname,thmname) =
     if !SkipProof.quick_and_dirty
--- a/src/HOL/Import/shuffler.ML	Sat May 29 16:50:53 2004 +0200
+++ b/src/HOL/Import/shuffler.ML	Mon May 31 08:53:23 2004 +0200
@@ -58,8 +58,8 @@
 (*Prints an exception, then fails*)
 fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
 
-val string_of_thm = Library.setmp print_mode [] (Output.output o string_of_thm);
-val string_of_cterm = Library.setmp print_mode [] (Output.output o string_of_cterm);
+val string_of_thm = Library.setmp print_mode [] string_of_thm;
+val string_of_cterm = Library.setmp print_mode [] string_of_cterm;
 
 fun mk_meta_eq th =
     (case concl_of th of
isabelle