src/Pure/meta_simplifier.ML
changeset 11886 36d0585f87de
parent 11767 7380c9d45626
child 12155 13c5469b4bb3
     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*)