# HG changeset patch
# User wenzelm
# Date 1630876892 -7200
# Node ID 36774e8af3db272b9e0fead3633a632e1cfd9a10
# Parent  914a214e110e8a0b22418d7b1748b35361c715af
more robust signature: result has no particular order;

diff -r 914a214e110e -r 36774e8af3db src/Doc/Implementation/Proof.thy
--- a/src/Doc/Implementation/Proof.thy	Sun Sep 05 21:09:31 2021 +0200
+++ b/src/Doc/Implementation/Proof.thy	Sun Sep 05 23:21:32 2021 +0200
@@ -101,7 +101,7 @@
   @{define_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
   @{define_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
   @{define_ML Variable.import: "bool -> thm list -> Proof.context ->
-  ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list)
+  ((ctyp Term_Subst.TVars.table * cterm Term_Subst.Vars.table) * thm list)
     * Proof.context"} \\
   @{define_ML Variable.focus: "binding list option -> term -> Proof.context ->
   ((string * (string * typ)) list * term) * Proof.context"} \\
diff -r 914a214e110e -r 36774e8af3db src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sun Sep 05 21:09:31 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sun Sep 05 23:21:32 2021 +0200
@@ -870,8 +870,8 @@
     val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
     fun rewrite_pat (ct1, ct2) =
       (ct1, Thm.cterm_of ctxt3 (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
-    val t_insts' = map rewrite_pat t_insts
-    val intro'' = Thm.instantiate (T_insts, t_insts') intro
+    val t_insts' = map rewrite_pat (Term_Subst.Vars.dest t_insts)
+    val intro'' = Thm.instantiate (Term_Subst.TVars.dest T_insts, t_insts') intro
     val [intro'''] = Variable.export ctxt3 ctxt [intro'']
     val intro'''' =
       Simplifier.full_simplify
diff -r 914a214e110e -r 36774e8af3db src/Pure/Isar/subgoal.ML
--- a/src/Pure/Isar/subgoal.ML	Sun Sep 05 21:09:31 2021 +0200
+++ b/src/Pure/Isar/subgoal.ML	Sun Sep 05 23:21:32 2021 +0200
@@ -58,7 +58,7 @@
     val ((_, inst), ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
     val schematic_terms = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst [];
 
-    val schematics = (schematic_types, schematic_terms);
+    val schematics = (Term_Subst.TVars.dest schematic_types, schematic_terms);
     val asms' = map (Thm.instantiate_cterm schematics) asms;
     val concl' = Thm.instantiate_cterm schematics concl;
     val (prems, context) = Assumption.add_assumes asms' ctxt3;
diff -r 914a214e110e -r 36774e8af3db src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sun Sep 05 21:09:31 2021 +0200
+++ b/src/Pure/variable.ML	Sun Sep 05 23:21:32 2021 +0200
@@ -74,11 +74,10 @@
     (typ Term_Subst.TVars.table * term Term_Subst.Vars.table) * Proof.context
   val importT_terms: term list -> Proof.context -> term list * Proof.context
   val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
-  val importT: thm list -> Proof.context ->
-    (((indexname * sort) * ctyp) list * thm list) * Proof.context
+  val importT: thm list -> Proof.context -> (ctyp Term_Subst.TVars.table * thm list) * Proof.context
   val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
   val import: bool -> thm list -> Proof.context ->
-    ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context
+    ((ctyp Term_Subst.TVars.table * cterm Term_Subst.Vars.table) * thm list) * Proof.context
   val import_vars: Proof.context -> thm -> thm
   val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
@@ -620,8 +619,8 @@
 fun importT ths ctxt =
   let
     val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
-    val instT' = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T)) instT [];
-    val ths' = map (Thm.instantiate (instT', [])) ths;
+    val instT' = Term_Subst.TVars.map (K (Thm.ctyp_of ctxt')) instT;
+    val ths' = map (Thm.instantiate (Term_Subst.TVars.dest instT', [])) ths;
   in ((instT', ths'), ctxt') end;
 
 fun import_prf is_open prf ctxt =
@@ -633,9 +632,9 @@
 fun import is_open ths ctxt =
   let
     val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
-    val instT' = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T)) instT [];
-    val inst' = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt' t)) inst [];
-    val ths' = map (Thm.instantiate (instT', inst')) ths;
+    val instT' = Term_Subst.TVars.map (K (Thm.ctyp_of ctxt')) instT;
+    val inst' = Term_Subst.Vars.map (K (Thm.cterm_of ctxt')) inst;
+    val ths' = map (Thm.instantiate (Term_Subst.TVars.dest instT', Term_Subst.Vars.dest inst')) ths;
   in (((instT', inst'), ths'), ctxt') end;
 
 fun import_vars ctxt th =