--- a/src/HOL/Import/shuffler.ML Fri May 16 23:25:37 2008 +0200
+++ b/src/HOL/Import/shuffler.ML Sat May 17 13:54:30 2008 +0200
@@ -42,7 +42,7 @@
case e of
THM (msg,i,thms) =>
(writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
- List.app print_thm thms)
+ List.app Display.print_thm thms)
| THEORY (msg,thys) =>
(writeln ("Exception THEORY raised:\n" ^ msg);
List.app (writeln o Context.str_of_thy) thys)
@@ -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 = PrintMode.setmp [] string_of_thm;
-val string_of_cterm = PrintMode.setmp [] string_of_cterm;
+val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
+val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm;
fun mk_meta_eq th =
(case concl_of th of
@@ -305,11 +305,11 @@
in
if not (lhs aconv origt)
then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
- writeln (string_of_cterm (cterm_of thy origt));
- writeln (string_of_cterm (cterm_of thy lhs));
- writeln (string_of_cterm (cterm_of thy typet));
- writeln (string_of_cterm (cterm_of thy t));
- app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
+ writeln (Display.string_of_cterm (cterm_of thy origt));
+ writeln (Display.string_of_cterm (cterm_of thy lhs));
+ writeln (Display.string_of_cterm (cterm_of thy typet));
+ writeln (Display.string_of_cterm (cterm_of thy t));
+ app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst;
writeln "done")
else ()
end
@@ -367,11 +367,11 @@
in
if not (lhs aconv origt)
then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
- writeln (string_of_cterm (cterm_of thy origt));
- writeln (string_of_cterm (cterm_of thy lhs));
- writeln (string_of_cterm (cterm_of thy typet));
- writeln (string_of_cterm (cterm_of thy t));
- app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
+ writeln (Display.string_of_cterm (cterm_of thy origt));
+ writeln (Display.string_of_cterm (cterm_of thy lhs));
+ writeln (Display.string_of_cterm (cterm_of thy typet));
+ writeln (Display.string_of_cterm (cterm_of thy t));
+ app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst;
writeln "done")
else ()
end