src/Pure/old_goals.ML
changeset 26939 1035c89b4c02
parent 26928 ca87aff1ad2d
child 27157 0ddb5576b387
     1.1 --- a/src/Pure/old_goals.ML	Sat May 17 23:53:20 2008 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Sun May 18 15:04:09 2008 +0200
     1.3 @@ -182,7 +182,7 @@
     1.4                  (string_of_int ngoals ^ " unsolved goals!")
     1.5              else if not (null hyps) then !result_error_fn state
     1.6                  ("Additional hypotheses:\n" ^
     1.7 -                 cat_lines (map (Sign.string_of_term thy) hyps))
     1.8 +                 cat_lines (map (Syntax.string_of_term_global thy) hyps))
     1.9              else if Pattern.matches thy
    1.10                                      (Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
    1.11                   then final_th
    1.12 @@ -207,11 +207,11 @@
    1.13            List.app (writeln o Context.str_of_thy) thys)
    1.14     | TERM (msg,ts) =>
    1.15           (writeln ("Exception TERM raised:\n" ^ msg);
    1.16 -          List.app (writeln o Sign.string_of_term thy) ts)
    1.17 +          List.app (writeln o Syntax.string_of_term_global thy) ts)
    1.18     | TYPE (msg,Ts,ts) =>
    1.19           (writeln ("Exception TYPE raised:\n" ^ msg);
    1.20 -          List.app (writeln o Sign.string_of_typ thy) Ts;
    1.21 -          List.app (writeln o Sign.string_of_term thy) ts)
    1.22 +          List.app (writeln o Syntax.string_of_typ_global thy) Ts;
    1.23 +          List.app (writeln o Syntax.string_of_term_global thy) ts)
    1.24     | e => raise e;
    1.25  
    1.26  (*Prints an exception, then fails*)