# HG changeset patch
# User wenzelm
# Date 1526841100 -7200
# Node ID 07eb13eb40657875d8c3c86e53be64cac34295de
# Parent  5e0e9376b2b045b091997b6efee00efcb02d48bd
tuned signature;

diff -r 5e0e9376b2b0 -r 07eb13eb4065 src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Sun May 20 18:45:18 2018 +0200
+++ b/src/Pure/term_subst.ML	Sun May 20 20:31:40 2018 +0200
@@ -29,9 +29,10 @@
   val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
   val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
     term -> term
-  val zero_var_indexes: term -> term
   val zero_var_indexes_inst: term list ->
     ((indexname * sort) * typ) list * ((indexname * typ) * term) list
+  val zero_var_indexes: term -> term
+  val zero_var_indexes_list: term list -> term list
 end;
 
 structure Term_Subst: TERM_SUBST =
@@ -224,6 +225,7 @@
         ([], Name.context);
   in (instT, inst) end;
 
-fun zero_var_indexes t = instantiate (zero_var_indexes_inst [t]) t;
+fun zero_var_indexes_list ts = map (instantiate (zero_var_indexes_inst ts)) ts;
+val zero_var_indexes = singleton zero_var_indexes_list;
 
 end;