1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Wed Jun 03 09:56:24 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Wed Jun 03 11:25:19 2020 +0200
     1.3 @@ -273,8 +273,8 @@
     1.4        | scan vs (Bound _) = vs 
     1.5        | scan vs (Abs (_, _, t)) = scan vs t
     1.6        | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
     1.7 -  in (distinct o (scan [])) t end;
     1.8 -fun vars' ts = ts |> map vars |> flat |> distinct
     1.9 +  in ((distinct op =) o (scan [])) t end;
    1.10 +fun vars' ts = ts |> map vars |> flat |> distinct op =
    1.11  
    1.12  (* bypass Isabelle's Pretty, which requires ctxt *)
    1.13  fun ids2str t =
    1.14 @@ -285,7 +285,7 @@
    1.15        | scan vs (Bound _) = vs 
    1.16        | scan vs (Abs (s, _, t)) = scan (s :: vs) t
    1.17        | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
    1.18 -  in (distinct o (scan [])) t end;
    1.19 +  in ((distinct op =) o (scan [])) t end;
    1.20  fun is_bdv str = case Symbol.explode str of "b"::"d"::"v"::_ => true | _ => false;
    1.21  (* instantiate #prop thm with bound variables (as Free) *)
    1.22  fun inst_bdv [] t = t
    1.23 @@ -579,7 +579,7 @@
    1.24  fun vars_of t =
    1.25    let
    1.26      val var_ids = t |> ids2str |> subtract op = poly_consts |> map strip_thy |> sort string_ord
    1.27 -  in (map (var_for [] t) var_ids) |> flat |> distinct end
    1.28 +  in (map (var_for [] t) var_ids) |> flat |> distinct op = end
    1.29  
    1.30  (* this may decompose an object-language isa-list;
    1.31     use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*)