# HG changeset patch
# User wenzelm
# Date 1128001846 -7200
# Node ID ee5b42e3cbb4243560bce0e355ded0736dc01254
# Parent  8e098e040c2e6f805e2d5808bfeed4c9a3b7ec6c
export debug_bounds;

diff -r 8e098e040c2e -r ee5b42e3cbb4 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu Sep 29 15:50:45 2005 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Sep 29 15:50:46 2005 +0200
@@ -81,6 +81,7 @@
     -> (theory -> simpset -> term -> thm option) -> simproc
   val simproc: theory -> string -> string list
     -> (theory -> simpset -> term -> thm option) -> simproc
+  val debug_bounds: bool ref
   val inherit_bounds: simpset -> simpset -> simpset
   val rewrite_cterm: bool * bool * bool ->
     (simpset -> thm -> thm option) -> simpset -> cterm -> thm
@@ -1122,7 +1123,7 @@
       | _ => I) (term_of ct) [];
   in
     if null bs then ()
-    else print_term true ("Simplifier: term contains loose bounds: " ^ commas bs) ss
+    else print_term true ("Simplifier: term contains loose bounds: " ^ commas_quote bs) ss
       (Thm.theory_of_cterm ct) (Thm.term_of ct)
   end);
 
diff -r 8e098e040c2e -r ee5b42e3cbb4 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Sep 29 15:50:45 2005 +0200
+++ b/src/Pure/simplifier.ML	Thu Sep 29 15:50:46 2005 +0200
@@ -53,6 +53,7 @@
 sig
   include BASIC_SIMPLIFIER
   val clear_ss: simpset -> simpset
+  val debug_bounds: bool ref
   val inherit_bounds: simpset -> simpset -> simpset
   val simproc_i: theory -> string -> term list
     -> (theory -> simpset -> term -> thm option) -> simproc