diff -r bcd14373ec30 -r 64f30bdd3ba1 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Fri Aug 28 18:23:24 2009 +0200
+++ b/src/HOL/Import/shuffler.ML	Fri Aug 28 21:04:03 2009 +0200
@@ -57,7 +57,6 @@
 fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
 
 val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context;
-val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm;
 
 fun mk_meta_eq th =
     (case concl_of th of
@@ -304,13 +303,14 @@
                 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 (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")
+                then
+                  writeln (cat_lines
+                    (["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)",
+                      Syntax.string_of_term_global thy origt,
+                      Syntax.string_of_term_global thy lhs,
+                      Syntax.string_of_term_global thy typet,
+                      Syntax.string_of_term_global thy t] @
+                      map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst))
                 else ()
             end
     in
@@ -366,13 +366,14 @@
                 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 (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")
+                then
+                  writeln (cat_lines
+                    (["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)",
+                      Syntax.string_of_term_global thy origt,
+                      Syntax.string_of_term_global thy lhs,
+                      Syntax.string_of_term_global thy typet,
+                      Syntax.string_of_term_global thy t] @
+                      map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst))
                 else ()
             end
     in
@@ -407,9 +408,8 @@
                       end
                     | _ => NONE)
             else NONE
-          | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE)
-    end
-    handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
+          | _ => error ("Bad eta_expand argument" ^ Syntax.string_of_term_global thy t)
+    end;
 
 fun mk_tfree s = TFree("'"^s,[])
 fun mk_free s t = Free (s,t)