# HG changeset patch
# User wenzelm
# Date 1635099951 -7200
# Node ID 7625b5d7cfe2cd7dfa848ef3a624497127a50529
# Parent  f4613ca298e6aba075c58614da12bebcf91ae346
clarified name, syntax, messages;

diff -r f4613ca298e6 -r 7625b5d7cfe2 etc/symbols
--- a/etc/symbols	Sun Oct 24 18:29:21 2021 +0200
+++ b/etc/symbols	Sun Oct 24 20:25:51 2021 +0200
@@ -455,8 +455,8 @@
 \<^cprop>               argument: cartouche
 \<^cterm>               argument: cartouche
 \<^ctyp>                argument: cartouche
+\<^instantiate>         argument: cartouche
 \<^keyword>             argument: cartouche
-\<^let>                 argument: cartouche
 \<^locale>              argument: cartouche
 \<^make_judgment>
 \<^dest_judgment>
diff -r f4613ca298e6 -r 7625b5d7cfe2 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Sun Oct 24 18:29:21 2021 +0200
+++ b/lib/texinputs/isabellesym.sty	Sun Oct 24 20:25:51 2021 +0200
@@ -444,9 +444,9 @@
 \newcommand{\isactrldir}{\isakeywordcontrol{dir}}
 \newcommand{\isactrlfile}{\isakeywordcontrol{file}}
 \newcommand{\isactrlhere}{\isakeywordcontrol{here}}
+\newcommand{\isactrlinstantiate}{\isakeywordcontrol{instantiate}}
 \newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}}
 \newcommand{\isactrllatex}{\isakeywordcontrol{latex}}
-\newcommand{\isactrllet}{\isakeywordcontrol{let}}
 \newcommand{\isactrllocale}{\isakeywordcontrol{locale}}
 \newcommand{\isactrlmakeUNDERSCOREjudgment}{\isakeywordcontrol{make{\isacharunderscore}judgment}}
 \newcommand{\isactrldestUNDERSCOREjudgment}{\isakeywordcontrol{dest{\isacharunderscore}judgment}}
diff -r f4613ca298e6 -r 7625b5d7cfe2 src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Oct 24 18:29:21 2021 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Oct 24 20:25:51 2021 +0200
@@ -660,7 +660,7 @@
 local
 
 fun pol (ctxt, ct, t) =
-  \<^let>\<open>x = ct and y = \<open>Thm.cterm_of ctxt t\<close>
+  \<^instantiate>\<open>x = ct and y = \<open>Thm.cterm_of ctxt t\<close>
     in cterm \<open>x \<equiv> y\<close> for x y :: pol\<close>;
 
 val (_, raw_pol_oracle) = Context.>>> (Context.map_theory_result
diff -r f4613ca298e6 -r 7625b5d7cfe2 src/HOL/Decision_Procs/Reflective_Field.thy
--- a/src/HOL/Decision_Procs/Reflective_Field.thy	Sun Oct 24 18:29:21 2021 +0200
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy	Sun Oct 24 20:25:51 2021 +0200
@@ -640,7 +640,7 @@
 local
 
 fun fnorm (ctxt, ct, t) =
-  \<^let>\<open>x = ct and y = \<open>Thm.cterm_of ctxt t\<close>
+  \<^instantiate>\<open>x = ct and y = \<open>Thm.cterm_of ctxt t\<close>
     in cterm \<open>x \<equiv> y\<close> for x y :: \<open>pexpr \<times> pexpr \<times> pexpr list\<close>\<close>;
 
 val (_, raw_fnorm_oracle) = Context.>>> (Context.map_theory_result
@@ -881,7 +881,7 @@
       val cxs = Thm.cterm_of ctxt (HOLogic.mk_list T (map Free xs));
       val ce = Thm.cterm_of ctxt (reif xs t);
       val ce' = Thm.cterm_of ctxt (reif xs u);
-      val fnorm = cv ctxt \<^let>\<open>e = ce and e' = ce' in cterm \<open>fnorm (FSub e e')\<close>\<close>;
+      val fnorm = cv ctxt \<^instantiate>\<open>e = ce and e' = ce' in cterm \<open>fnorm (FSub e e')\<close>\<close>;
       val (_, [n, dc]) = strip_app (Thm.rhs_of fnorm);
       val (_, [_, c]) = strip_app dc;
       val th =
diff -r f4613ca298e6 -r 7625b5d7cfe2 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Sun Oct 24 18:29:21 2021 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Sun Oct 24 20:25:51 2021 +0200
@@ -81,7 +81,7 @@
   | _ => [ct]);
 
 val list_conj =
-  foldr1 (fn (A, B) => \<^let>\<open>A = A and B = B in cterm \<open>A \<and> B\<close>\<close>);
+  foldr1 (fn (A, B) => \<^instantiate>\<open>A and B in cterm \<open>A \<and> B\<close>\<close>);
 
 fun mk_conj_tab th =
   let
@@ -144,7 +144,7 @@
                 [] => NONE
               | _ =>
                 conj_aci_rule
-                  \<^let>\<open>A = p and B = \<open>list_conj (ndx @ dx)\<close> in cterm \<open>Trueprop A \<equiv> Trueprop B\<close>\<close>
+                  \<^instantiate>\<open>A = p and B = \<open>list_conj (ndx @ dx)\<close> in cterm \<open>Trueprop A \<equiv> Trueprop B\<close>\<close>
                 |> Thm.abstract_rule xn x
                 |> Drule.arg_cong_rule e
                 |> Conv.fconv_rule
@@ -155,7 +155,7 @@
             end
         | _ =>
             conj_aci_rule
-              \<^let>\<open>A = p and B = \<open>list_conj (eqs @ neqs)\<close> in cterm \<open>Trueprop A \<equiv> Trueprop B\<close>\<close>
+              \<^instantiate>\<open>A = p and B = \<open>list_conj (eqs @ neqs)\<close> in cterm \<open>Trueprop A \<equiv> Trueprop B\<close>\<close>
             |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
             |> Conv.fconv_rule
                 (Conv.arg_conv
diff -r f4613ca298e6 -r 7625b5d7cfe2 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Sun Oct 24 18:29:21 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Sun Oct 24 20:25:51 2021 +0200
@@ -255,9 +255,12 @@
   |> Keyword.no_major_keywords
   |> Keyword.add_major_keywords ["typ", "term", "prop", "ctyp", "cterm", "cprop"];
 
+val parse_inst_name = Parse.position (Parse.type_ident >> pair true || Parse.name >> pair false);
+
 val parse_inst =
-  Parse.position (Parse.type_ident >> pair true || Parse.name >> pair false) --
-    (Parse.$$$ "=" |-- Parse.!!! Parse.embedded_ml) >> (fn (((b, a), pos), ml) => (b, ((a, pos), ml)));
+  (parse_inst_name -- (Parse.$$$ "=" |-- Parse.!!! Parse.embedded_ml) ||
+    Scan.ahead parse_inst_name -- Parse.embedded_ml)
+  >> (fn (((b, a), pos), ml) => (b, ((a, pos), ml)));
 
 val parse_insts =
   Parse.and_list1 parse_inst >> (List.partition #1 #> apply2 (map #2));
@@ -274,12 +277,12 @@
 fun get_tfree envT (a, pos) =
   (case AList.lookup (op =) envT a of
     SOME S => (a, S)
-  | NONE => error ("Unused type variable " ^ quote a ^ Position.here pos));
+  | NONE => error ("No occurrence of type variable " ^ quote a ^ Position.here pos));
 
 fun get_free env (x, pos) =
   (case AList.lookup (op =) env x of
     SOME T => (x, T)
-  | NONE => error ("Unused variable " ^ quote x ^ Position.here pos));
+  | NONE => error ("No occurrence of variable " ^ quote x ^ Position.here pos));
 
 fun make_instT (a, pos) T =
   (case try (Term.dest_TVar o Logic.dest_type) T of
@@ -343,7 +346,7 @@
     -- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_prop range;
 
 val _ = Theory.setup
-  (ML_Context.add_antiquotation \<^binding>\<open>let\<close> true
+  (ML_Context.add_antiquotation \<^binding>\<open>instantiate\<close> true
     (fn range => fn src => fn ctxt =>
       let
         val (insts, prepare_val) = src