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.
tuned error message: regular Pretty.string_of instead of raw Pretty.output;
authorwenzelm
Sat, 08 May 2010 19:18:28 +0200
changeset 36746 6e7704471eaa
parent 36745 403585a89772
child 36747 7361d5dde9ce
tuned error message: regular Pretty.string_of instead of raw Pretty.output;
src/Pure/Isar/class.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/class.ML	Sat May 08 19:14:13 2010 +0200
+++ b/src/Pure/Isar/class.ML	Sat May 08 19:18:28 2010 +0200
@@ -202,7 +202,7 @@
       |> Expression.cert_declaration supexpr I inferred_elems;
     fun check_vars e vs = if null vs
       then error ("No type variable in part of specification element "
-        ^ (Pretty.output NONE o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))
+        ^ (Pretty.string_of o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))
       else ();
     fun check_element (e as Element.Fixes fxs) =
           map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs
isabelle