Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
export debug_bounds;
authorwenzelm
Thu, 29 Sep 2005 15:50:46 +0200
changeset 17723 ee5b42e3cbb4
parent 17722 8e098e040c2e
child 17724 e969fc0a4925
export debug_bounds;
src/Pure/meta_simplifier.ML file | annotate | diff | comparison | revisions
src/Pure/simplifier.ML file | annotate | diff | comparison | revisions 
--- 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);
 
--- 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
isabelle