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/sign.ML
changeset 37145 01aa36932739
parent 36610 bafd82950e24
child 39133 70d3915c92f0 
--- a/src/Pure/sign.ML	Thu May 27 15:28:23 2010 +0200
+++ b/src/Pure/sign.ML	Thu May 27 17:41:27 2010 +0200
@@ -271,7 +271,7 @@
         val t' = subst_bounds (xs, t);
         val u' = subst_bounds (xs, u);
         val msg = cat_lines
-          (TypeInfer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
+          (Type_Infer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
       in raise TYPE (msg, [T, U], [t', u']) end;
 
     fun typ_of (_, Const (_, T)) = T
isabelle