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/Syntax/syntax_phases.ML
changeset 55951 c07d184aebe9
parent 55950 3bb5c7179234
child 55953 b19373bd7ea8 
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 11:32:16 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 12:10:19 2014 +0100
@@ -170,7 +170,8 @@
           let
             val pos = Lexicon.pos_of_token tok;
             val (Type (c, _), rs) =
-              Proof_Context.check_type_name_proper ctxt false (Lexicon.str_of_token tok, pos);
+              Proof_Context.check_type_name ctxt {proper = true, strict = false}
+                (Lexicon.str_of_token tok, pos);
             val _ = Unsynchronized.change reports (append (map (rpair "") rs));
           in [Ast.Constant (Lexicon.mark_type c)] end
       | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
isabelle