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