tuned signature;
authorwenzelm
Sun May 20 20:31:40 2018 +0200 (21 months ago)
changeset 6823407eb13eb4065
parent 68233 5e0e9376b2b0
child 68235 a3bd410db5b2
tuned signature;
src/Pure/term_subst.ML
     1.1 --- a/src/Pure/term_subst.ML	Sun May 20 18:45:18 2018 +0200
     1.2 +++ b/src/Pure/term_subst.ML	Sun May 20 20:31:40 2018 +0200
     1.3 @@ -29,9 +29,10 @@
     1.4    val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
     1.5    val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
     1.6      term -> term
     1.7 -  val zero_var_indexes: term -> term
     1.8    val zero_var_indexes_inst: term list ->
     1.9      ((indexname * sort) * typ) list * ((indexname * typ) * term) list
    1.10 +  val zero_var_indexes: term -> term
    1.11 +  val zero_var_indexes_list: term list -> term list
    1.12  end;
    1.13  
    1.14  structure Term_Subst: TERM_SUBST =
    1.15 @@ -224,6 +225,7 @@
    1.16          ([], Name.context);
    1.17    in (instT, inst) end;
    1.18  
    1.19 -fun zero_var_indexes t = instantiate (zero_var_indexes_inst [t]) t;
    1.20 +fun zero_var_indexes_list ts = map (instantiate (zero_var_indexes_inst ts)) ts;
    1.21 +val zero_var_indexes = singleton zero_var_indexes_list;
    1.22  
    1.23  end;