src/HOL/Import/shuffler.ML
changeset 26928 ca87aff1ad2d
parent 26690 e30b8d500c7d
child 26939 1035c89b4c02
     1.1 --- a/src/HOL/Import/shuffler.ML	Fri May 16 23:25:37 2008 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Sat May 17 13:54:30 2008 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4    case e of
     1.5       THM (msg,i,thms) =>
     1.6           (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
     1.7 -          List.app print_thm thms)
     1.8 +          List.app Display.print_thm thms)
     1.9     | THEORY (msg,thys) =>
    1.10           (writeln ("Exception THEORY raised:\n" ^ msg);
    1.11            List.app (writeln o Context.str_of_thy) thys)
    1.12 @@ -58,8 +58,8 @@
    1.13  (*Prints an exception, then fails*)
    1.14  fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
    1.15  
    1.16 -val string_of_thm = PrintMode.setmp [] string_of_thm;
    1.17 -val string_of_cterm = PrintMode.setmp [] string_of_cterm;
    1.18 +val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
    1.19 +val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm;
    1.20  
    1.21  fun mk_meta_eq th =
    1.22      (case concl_of th of
    1.23 @@ -305,11 +305,11 @@
    1.24              in
    1.25                  if not (lhs aconv origt)
    1.26                  then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
    1.27 -                      writeln (string_of_cterm (cterm_of thy origt));
    1.28 -                      writeln (string_of_cterm (cterm_of thy lhs));
    1.29 -                      writeln (string_of_cterm (cterm_of thy typet));
    1.30 -                      writeln (string_of_cterm (cterm_of thy t));
    1.31 -                      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
    1.32 +                      writeln (Display.string_of_cterm (cterm_of thy origt));
    1.33 +                      writeln (Display.string_of_cterm (cterm_of thy lhs));
    1.34 +                      writeln (Display.string_of_cterm (cterm_of thy typet));
    1.35 +                      writeln (Display.string_of_cterm (cterm_of thy t));
    1.36 +                      app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst;
    1.37                        writeln "done")
    1.38                  else ()
    1.39              end
    1.40 @@ -367,11 +367,11 @@
    1.41              in
    1.42                  if not (lhs aconv origt)
    1.43                  then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
    1.44 -                      writeln (string_of_cterm (cterm_of thy origt));
    1.45 -                      writeln (string_of_cterm (cterm_of thy lhs));
    1.46 -                      writeln (string_of_cterm (cterm_of thy typet));
    1.47 -                      writeln (string_of_cterm (cterm_of thy t));
    1.48 -                      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
    1.49 +                      writeln (Display.string_of_cterm (cterm_of thy origt));
    1.50 +                      writeln (Display.string_of_cterm (cterm_of thy lhs));
    1.51 +                      writeln (Display.string_of_cterm (cterm_of thy typet));
    1.52 +                      writeln (Display.string_of_cterm (cterm_of thy t));
    1.53 +                      app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst;
    1.54                        writeln "done")
    1.55                  else ()
    1.56              end