Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature;
authorwenzelm
Sun, 20 May 2018 20:31:40 +0200
changeset 68234 07eb13eb4065
parent 68233 5e0e9376b2b0
child 68235 a3bd410db5b2
tuned signature;
src/Pure/term_subst.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle