# HG changeset patch
# User wenzelm
# Date 1635446301 -7200
# Node ID 6676bf1898526807812ba2087910291cd4ecd23e
# Parent  54085e37ce4d047d495806534340b4a1ccc5bc23
discontinued somewhat pointless antiquotations;

diff -r 54085e37ce4d -r 6676bf189852 NEWS
--- 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.
diff -r 54085e37ce4d -r 6676bf189852 src/Pure/ML/ml_antiquotations.ML
--- 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) =>
diff -r 54085e37ce4d -r 6676bf189852 src/ZF/Tools/inductive_package.ML
--- 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}));