1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Tue May 19 12:33:35 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Wed May 20 12:52:09 2020 +0200
1.3 @@ -152,7 +152,7 @@
1.4 enclose "TFree(" ")" (quote s ^ ", " ^ (sort |> map quote |> commas |> enclose "List(" ")"))
1.5 | scala_of_typ (TVar ((s, i), sort)) =
1.6 enclose "TVar(" ")" (
1.7 - enclose "(" ")," (quote s ^ "," ^ quote (string_of_int i)) ^
1.8 + enclose "(" ")," (quote s ^ ", " ^ quote (string_of_int i)) ^
1.9 (sort |> map quote |> commas |> enclose "List(" ")"))
1.10 fun scala_of_term (Const (s, T)) =
1.11 enclose "Const(" ")" (quote s ^ ", " ^ scala_of_typ T)
1.12 @@ -160,7 +160,7 @@
1.13 enclose "Free(" ")" (quote s ^ ", " ^ scala_of_typ T)
1.14 | scala_of_term (Var ((s, i), T)) =
1.15 enclose "TVar(" ")" (
1.16 - enclose "(" ")," (quote s ^ "," ^ quote (string_of_int i)) ^
1.17 + enclose "(" ")," (quote s ^ ", " ^ quote (string_of_int i)) ^
1.18 scala_of_typ T)
1.19 | scala_of_term (Bound i) = enclose "Bound(" ")" (string_of_int i)
1.20 | scala_of_term (Abs (s, T, t)) =
1.21 @@ -177,9 +177,9 @@
1.22 let
1.23 fun ato n (Type (s, [])) = "\n*** " ^ indent n ^ "Type (" ^ s ^",[])"
1.24 | ato n (Type (s, Ts)) = "\n*** " ^ indent n ^ "Type (" ^ s ^ ",[" ^ atol (n + 1) Ts
1.25 - | ato n (TFree (s, sort)) = "\n*** " ^ indent n ^ "TFree (" ^ s ^ "," ^ strs2str' sort
1.26 + | ato n (TFree (s, sort)) = "\n*** " ^ indent n ^ "TFree (" ^ s ^ ", " ^ strs2str' sort
1.27 | ato n (TVar ((s, i), sort)) =
1.28 - "\n*** " ^ indent n ^ "TVar ((" ^ s ^ "," ^ string_of_int i ^ strs2str' sort
1.29 + "\n*** " ^ indent n ^ "TVar ((" ^ s ^ ", " ^ string_of_int i ^ strs2str' sort
1.30 and atol n [] = "\n*** " ^ indent n ^ "]"
1.31 | atol n (T :: Ts) = (ato n T ^ atol n Ts)
1.32 in tracing (ato 0 t ^ "\n") end;