src/HOL/Import/shuffler.ML

 (*Prints exceptions readably to users*)
 fun print_sign_exn_unit sign e =
   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)
    | TERM (msg,ts) =>
          (writeln ("Exception TERM raised:\n" ^ msg);

    | e => raise e
 
 (*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
          Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection
        | Const("==",_) $ _ $ _ => th

             let
                 val lhs = #1 (Logic.dest_equals (prop_of (final init)))
             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
     in
         case t of

             let
                 val lhs = #1 (Logic.dest_equals (prop_of (final init)))
             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
     in
         case t of