src/Pure/global_theory.ML
changeset 42381 309ec68442c6
parent 42379 26f64dddf2c6
child 42471 593289343c7d
--- a/src/Pure/global_theory.ML	Sun Apr 17 21:17:45 2011 +0200
+++ b/src/Pure/global_theory.ML	Sun Apr 17 21:42:47 2011 +0200
@@ -205,7 +205,7 @@
 
 fun read ctxt (b, str) =
   Syntax.read_prop ctxt str handle ERROR msg =>
-    cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b));
+    cat_error msg ("The error(s) above occurred in definition " ^ Binding.print b);
 
 fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
   let