# HG changeset patch
# User wenzelm
# Date 1724582623 -7200
# Node ID 4641f0fdaa59585aadd63778a180eed4a31da0c1
# Parent  8f96e1329845348c1d82e8180e2194fd680bf587
proper flags (amending 1319c729c65d): abbrevs are allowed, free variables are disallowed;

diff -r 8f96e1329845 -r 4641f0fdaa59 src/Pure/Isar/isar_cmd.ML
--- 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