src/HOL/Import/shuffler.ML
changeset 26939 1035c89b4c02
parent 26928 ca87aff1ad2d
child 27173 9ae98c3cd3d6
     1.1 --- a/src/HOL/Import/shuffler.ML	Sat May 17 23:53:20 2008 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Sun May 18 15:04:09 2008 +0200
     1.3 @@ -48,11 +48,11 @@
     1.4            List.app (writeln o Context.str_of_thy) thys)
     1.5     | TERM (msg,ts) =>
     1.6           (writeln ("Exception TERM raised:\n" ^ msg);
     1.7 -          List.app (writeln o Sign.string_of_term sign) ts)
     1.8 +          List.app (writeln o Syntax.string_of_term_global sign) ts)
     1.9     | TYPE (msg,Ts,ts) =>
    1.10           (writeln ("Exception TYPE raised:\n" ^ msg);
    1.11 -          List.app (writeln o Sign.string_of_typ sign) Ts;
    1.12 -          List.app (writeln o Sign.string_of_term sign) ts)
    1.13 +          List.app (writeln o Syntax.string_of_typ_global sign) Ts;
    1.14 +          List.app (writeln o Syntax.string_of_term_global sign) ts)
    1.15     | e => raise e
    1.16  
    1.17  (*Prints an exception, then fails*)