--- 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>
--- 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}}
--- 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
--- 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 =
--- 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
--- 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