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/Statespace/distinct_tree_prover.ML
changeset 51701 1e29891759c4
parent 45740 132a3e1c0fe5
child 51717 9e7d1c139569 
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Fri Apr 12 14:54:14 2013 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Fri Apr 12 15:30:38 2013 +0200
@@ -107,9 +107,8 @@
     val insts' = map (apfst mapT_and_recertify) insts;
   in Thm.instantiate (instTs, insts') end;
 
-fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
-  quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
-  [TVar (ixn, S), TVar (ixn, S')], []);
+fun tvar_clash ixn S S' =
+  raise TYPE ("Type variable has two distinct sorts", [TVar (ixn, S), TVar (ixn, S')], []);
 
 fun lookup (tye, (ixn, S)) =
   (case AList.lookup (op =) tye ixn of
isabelle