Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/consts.ML
changeset 42381 309ec68442c6
parent 42375 774df7c59508
child 42383 0ae4ad40d7b5 
--- a/src/Pure/consts.ML	Sun Apr 17 21:17:45 2011 +0200
+++ b/src/Pure/consts.ML	Sun Apr 17 21:42:47 2011 +0200
@@ -275,7 +275,7 @@
     val force_expand = mode = Print_Mode.internal;
 
     val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
-      error ("Illegal schematic variables on rhs of abbreviation " ^ quote (Binding.str_of b));
+      error ("Illegal schematic variables on rhs of abbreviation " ^ Binding.print b);
 
     val rhs = raw_rhs
       |> Term.map_types (Type.cert_typ tsig)
isabelle