1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Wed May 20 12:52:09 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Sun May 24 16:05:36 2020 +0200
     1.3 @@ -89,7 +89,8 @@
     1.4  
     1.5    val var2free: term -> term
     1.6    val vars: term -> term list  (* recognises numverals, should replace "fun vars_of" *)
     1.7 -  val vars_of: term -> term list
     1.8 +  val vars': term list -> term list
     1.9 +  val vars_of: term -> term list   (* deprecated *)
    1.10    val dest_list': term -> term list
    1.11    val negates: term -> term -> bool
    1.12  
    1.13 @@ -273,6 +274,8 @@
    1.14        | scan vs (Abs (_, _, t)) = scan vs t
    1.15        | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
    1.16    in (distinct o (scan [])) t end;
    1.17 +fun vars' ts = ts |> map vars |> flat |> distinct
    1.18 +
    1.19  (* bypass Isabelle's Pretty, which requires ctxt *)
    1.20  fun ids2str t =
    1.21    let