Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper flags (amending 1319c729c65d): abbrevs are allowed, free variables are disallowed;
authorwenzelm
Sun, 25 Aug 2024 12:43:43 +0200
changeset 80759 4641f0fdaa59
parent 80758 8f96e1329845
child 80760 be8c0e039a5e
proper flags (amending 1319c729c65d): abbrevs are allowed, free variables are disallowed;
src/Pure/Isar/isar_cmd.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_cmd.ML	Sat Aug 24 23:44:05 2024 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Aug 25 12:43:43 2024 +0200
@@ -135,11 +135,11 @@
   in Sign.syntax_deps (maps check args) thy end;
 
 fun check_const ctxt (s, pos) =
-  Proof_Context.check_const {proper = false, strict = true} ctxt (s, [pos])
+  Proof_Context.check_const {proper = true, strict = false} ctxt (s, [pos])
   |>> (Term.dest_Const_name #> Lexicon.mark_const);
 
 fun check_type_name ctxt arg =
-  Proof_Context.check_type_name {proper = false, strict = true} ctxt arg
+  Proof_Context.check_type_name {proper = true, strict = false} ctxt arg
   |>> (Term.dest_Type_name #> Lexicon.mark_type);
 
 in
isabelle