Display.pretty_thms;
authorwenzelm
Mon Oct 22 18:01:38 2001 +0200 (2001-10-22)
changeset 1188636d0585f87de
parent 11885 427d80b807c7
child 11887 9a9da7969517
Display.pretty_thms;
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Mon Oct 22 18:01:26 2001 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Mon Oct 22 18:01:38 2001 +0200
     1.3 @@ -920,7 +920,7 @@
     1.4    end
     1.5    handle THM (s, _, thms) =>
     1.6      error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
     1.7 -      Pretty.string_of (pretty_thms thms));
     1.8 +      Pretty.string_of (Display.pretty_thms thms));
     1.9  
    1.10  (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
    1.11  (*Do not rewrite flex-flex pairs*)