1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Sun Aug 01 14:39:03 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Mon Aug 02 11:38:40 2021 +0200
     1.3 @@ -570,13 +570,10 @@
     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 (\<^const_name>\<open>numeral\<close>, _) $ _) = true
     1.8 -  | is_atom (Const (\<^const_name>\<open>one_class.one\<close>, _)) = true
     1.9 -  | is_atom (Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = true
    1.10 -  | is_atom (Const _) = true
    1.11 +fun is_atom (Const _) = true
    1.12    | is_atom (Free _) = true
    1.13    | is_atom (Var _) = true
    1.14 -  | is_atom _ = false;
    1.15 +  | is_atom t = is_num t;
    1.16  fun string_of_atom (t as Const (\<^const_name>\<open>numeral\<close>, _) $ _) = to_string t
    1.17    | string_of_atom (t as Const (\<^const_name>\<open>one_class.one\<close>, _)) = to_string t
    1.18    | string_of_atom (t as Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = to_string t