src/Tools/isac/BaseDefinitions/termC.sml
changeset 60266 4921574fd67f
parent 60226 9e005b89730b
child 60275 98ee674d18d3
     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 ()