--- 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)