1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Tue Jun 21 13:51:04 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Tue Jun 21 16:04:43 2022 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    val ids2str: term -> string list
     1.5    val ins_concl: term -> term -> term
     1.6    val inst_abs: term -> term
     1.7 -  val inst_bdv: (term * term) list -> term -> term
     1.8 +  val inst_bdv: LibraryC.subst -> term -> term
     1.9  
    1.10    val lhs: term -> term
    1.11    val rhs: term -> term
    1.12 @@ -83,7 +83,7 @@
    1.13    val str_of_int: int -> string
    1.14    val str2term: string -> term
    1.15    val strip_imp_prems': term -> term option
    1.16 -  val subst_atomic_all: (term * term) list -> term -> bool * term
    1.17 +  val subst_atomic_all: LibraryC.subst -> term -> bool * term
    1.18    val term_detail2str: term -> string
    1.19  
    1.20    val pairt: term -> term -> term
    1.21 @@ -341,7 +341,7 @@
    1.22    in ((distinct op =) o (scan [])) t
    1.23    end;
    1.24  fun is_bdv str = case Symbol.explode str of "b"::"d"::"v"::_ => true | _ => false;
    1.25 -(* instantiate #prop thm with bound variables (as Free) *)
    1.26 +(* instantiate #prop thm with bound vars_of (as Free) *)
    1.27  fun inst_bdv [] t = t
    1.28    | inst_bdv (instl: (term*term) list) t =
    1.29      let
    1.30 @@ -616,7 +616,7 @@
    1.31    [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>,
    1.32    \<^const_name>\<open>divide\<close>, \<^const_name>\<open>times\<close>,
    1.33    \<^const_name>\<open>realpow\<close>];
    1.34 -(* treat Free, Const, Var as variables in polynomials *)
    1.35 +(* treat Free, Const, Var as vars_of in polynomials *)
    1.36  fun vars_of t =
    1.37    let
    1.38      val var_ids = t |> ids2str |> subtract op = poly_consts |> map strip_thy |> sort string_ord