1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Fri May 07 13:23:24 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Fri May 07 18:12:51 2021 +0200
1.3 @@ -531,12 +531,6 @@
1.4 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
1.5
1.6 fun is_atom (Const ("Float.Float",_) $ _) = true
1.7 - | is_atom (Const ("ComplexI.I'_'_",_)) = true
1.8 - | is_atom (Const ("Groups.times_class.times",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t
1.9 - | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1
1.10 - | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $
1.11 - (Const ("Groups.times_class.times",_) $ t2 $ Const ("ComplexI.I'_'_",_))) =
1.12 - is_atom t1 andalso is_atom t2
1.13 | is_atom (Const _) = true
1.14 | is_atom (Free _) = true
1.15 | is_atom (Var _) = true