# HG changeset patch
# User wenzelm
# Date 1635175587 -7200
# Node ID 0b43d42cfde7ed82223062278cc22c9ee7a59628
# Parent  ccf599864beb85688ae496e181b341094e7398e1
tuned;

diff -r ccf599864beb -r 0b43d42cfde7 src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Mon Oct 25 11:41:03 2021 +0200
+++ b/src/Pure/term_subst.ML	Mon Oct 25 17:26:27 2021 +0200
@@ -13,13 +13,13 @@
   val generalize_same: Names.set * Names.set -> int -> term Same.operation
   val generalizeT: Names.set -> int -> typ -> typ
   val generalize: Names.set * Names.set -> int -> term -> term
-  val instantiateT_maxidx: (typ * int) TVars.table -> typ -> int -> typ * int
-  val instantiate_maxidx: (typ * int) TVars.table * (term * int) Vars.table ->
-    term -> int -> term * int
   val instantiateT_frees_same: typ TFrees.table -> typ Same.operation
   val instantiate_frees_same: typ TFrees.table * term Frees.table -> term Same.operation
   val instantiateT_frees: typ TFrees.table -> typ -> typ
   val instantiate_frees: typ TFrees.table * term Frees.table -> term -> term
+  val instantiateT_maxidx: (typ * int) TVars.table -> typ -> int -> typ * int
+  val instantiate_maxidx: (typ * int) TVars.table * (term * int) Vars.table ->
+    term -> int -> term * int
   val instantiateT_same: typ TVars.table -> typ Same.operation
   val instantiate_same: typ TVars.table * term Vars.table -> term Same.operation
   val instantiateT: typ TVars.table -> typ -> typ