--- a/NEWS Thu Oct 28 20:32:40 2021 +0200
+++ b/NEWS Thu Oct 28 20:38:21 2021 +0200
@@ -340,9 +340,6 @@
adoption; better use TVars.add, TVars.add_tfrees etc. for scalable
accumulation of items.
-* ML antiquotations \<^tvar>\<open>?'a::sort\<close> and \<^var>\<open>?x::type\<close> inline
-corresponding ML values, notably as arguments for Thm.instantiate etc.
-
* ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to
corresponding functions for the object-logic of the ML compilation
context. This supersedes older mk_Trueprop / dest_Trueprop operations.
--- a/src/Pure/ML/ml_antiquotations.ML Thu Oct 28 20:32:40 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Thu Oct 28 20:38:21 2021 +0200
@@ -94,26 +94,6 @@
ML_Syntax.print_string (Thm.check_oracle ctxt (name, pos)))));
-(* schematic variables *)
-
-val schematic_input =
- Args.context -- Scan.lift Parse.embedded_input >> (fn (ctxt, src) =>
- (Proof_Context.set_mode Proof_Context.mode_schematic ctxt,
- (Syntax.implode_input src, Input.pos_of src)));
-
-val _ = Theory.setup
- (ML_Antiquotation.inline_embedded \<^binding>\<open>tvar\<close>
- (schematic_input >> (fn (ctxt, (s, pos)) =>
- (case Syntax.read_typ ctxt s of
- TVar v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_sort v
- | _ => error ("Schematic type variable expected" ^ Position.here pos)))) #>
- ML_Antiquotation.inline_embedded \<^binding>\<open>var\<close>
- (schematic_input >> (fn (ctxt, (s, pos)) =>
- (case Syntax.read_term ctxt s of
- Var v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_typ v
- | _ => error ("Schematic variable expected" ^ Position.here pos)))));
-
-
(* type classes *)
fun class syn = Args.context -- Scan.lift Parse.embedded_inner_syntax >> (fn (ctxt, s) =>
--- a/src/ZF/Tools/inductive_package.ML Thu Oct 28 20:32:40 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML Thu Oct 28 20:38:21 2021 +0200
@@ -506,7 +506,7 @@
val inst =
case elem_frees of [_] => I
| _ => Drule.instantiate_normalize (TVars.empty,
- Vars.make [(\<^var>\<open>?x1::i\<close>, Thm.global_cterm_of thy4 elem_tuple)]);
+ Vars.make [((("x", 1), \<^Type>\<open>i\<close>), Thm.global_cterm_of thy4 elem_tuple)]);
(*strip quantifier and the implication*)
val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp}));