# HG changeset patch
# User wenzelm
# Date 1003766498 -7200
# Node ID 36d0585f87de72a4cd23512d8cb6ad92c75181bd
# Parent  427d80b807c74f1ca9f6efbdad96ad9511eef36f
Display.pretty_thms;

diff -r 427d80b807c7 -r 36d0585f87de src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon Oct 22 18:01:26 2001 +0200
+++ b/src/Pure/meta_simplifier.ML	Mon Oct 22 18:01:38 2001 +0200
@@ -920,7 +920,7 @@
   end
   handle THM (s, _, thms) =>
     error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
-      Pretty.string_of (pretty_thms thms));
+      Pretty.string_of (Display.pretty_thms thms));
 
 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
 (*Do not rewrite flex-flex pairs*)