src/Tools/isac/BaseDefinitions/termC.sml
changeset 60278 343efa173023
parent 60275 98ee674d18d3
child 60303 815b0dc8b589
child 60317 638d02a9a96a
     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