1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Wed Apr 28 12:38:13 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Thu Apr 29 09:55:06 2021 +0200
1.3 @@ -530,8 +530,6 @@
1.4 |> typ_a2real; (*TODO drop*)
1.5 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
1.6
1.7 -(* TODO decide with Test_Isac *)
1.8 -fun is_atom t = length (vars t) = 1
1.9 fun is_atom (Const ("Float.Float",_) $ _) = true
1.10 | is_atom (Const ("ComplexI.I'_'_",_)) = true
1.11 | is_atom (Const ("Groups.times_class.times",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t
1.12 @@ -597,7 +595,8 @@
1.13 fun raise_type_conflicts ts =
1.14 let
1.15 val dups = duplicates (op =) (map (fst o dest_Free) ts)
1.16 - val confl = filter (fn Free (str, _) => member op = dups str) ts
1.17 + val confl = filter (fn Free (str, _) => member op = dups str
1.18 + | _ => false) ts
1.19 in
1.20 if confl = []
1.21 then ()