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/envir.ML
changeset 51701 1e29891759c4
parent 51700 c8f2bad67dbb
child 51707 21d7933de1eb 
--- a/src/Pure/envir.ML	Fri Apr 12 14:54:14 2013 +0200
+++ b/src/Pure/envir.ML	Fri Apr 12 15:30:38 2013 +0200
@@ -106,8 +106,7 @@
   in (env', v) end;
 
 fun var_clash xi T T' =
-  raise TYPE ("Variable " ^ quote (Term.string_of_vname xi) ^ " has two distinct types",
-    [T', T], []);
+  raise TYPE ("Variable has two distinct types", [], [Var (xi, T'), Var (xi, T)]);
 
 fun lookup_check check tenv (xi, T) =
   (case Vartab.lookup tenv xi of
isabelle