src/Tools/isac/BaseDefinitions/termC.sml
changeset 60320 02102eaa2021
parent 60317 638d02a9a96a
child 60322 2220bafba61f
     1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Mon Jul 12 17:21:37 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Tue Jul 13 08:52:35 2021 +0200
     1.3 @@ -551,7 +551,9 @@
     1.4    |> typ_a2real;       (*TODO drop*)
     1.5  fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
     1.6  
     1.7 -fun is_atom (Const ("Float.Float",_) $ _) = true
     1.8 +fun is_atom (Const ("Num.numeral_class.numeral", _) $ _) = true
     1.9 +  | is_atom (Const ("Groups.one_class.one", _)) = true
    1.10 +  | is_atom (Const ("Groups.zero_class.zero", _)) = true
    1.11    | is_atom (Const _) = true
    1.12    | is_atom (Free _) = true
    1.13    | is_atom (Var _) = true