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/HOL/Tools/Quotient/quotient_def.ML
changeset 48992 0518bf89c777
parent 47938 2924f37cb6b3
child 50902 cb2b940e2fdf 
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Wed Aug 29 11:31:07 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Wed Aug 29 11:48:45 2012 +0200
@@ -48,7 +48,7 @@
 fun error_msg bind str =
   let
     val name = Binding.name_of bind
-    val pos = Position.str_of (Binding.pos_of bind)
+    val pos = Position.here (Binding.pos_of bind)
   in
     error ("Head of quotient_definition " ^
       quote str ^ " differs from declaration " ^ name ^ pos)
isabelle