diff -r e96abd81a321 -r f6e98785473f src/Tools/isac/BaseDefinitions/termC.sml
--- a/src/Tools/isac/BaseDefinitions/termC.sml	Sun Aug 01 14:39:03 2021 +0200
+++ b/src/Tools/isac/BaseDefinitions/termC.sml	Mon Aug 02 11:38:40 2021 +0200
@@ -570,13 +570,10 @@
   |> typ_a2real;       (*TODO drop*)
 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
 
-fun is_atom (Const (\<^const_name>\<open>numeral\<close>, _) $ _) = true
-  | is_atom (Const (\<^const_name>\<open>one_class.one\<close>, _)) = true
-  | is_atom (Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = true
-  | is_atom (Const _) = true
+fun is_atom (Const _) = true
   | is_atom (Free _) = true
   | is_atom (Var _) = true
-  | is_atom _ = false;
+  | is_atom t = is_num t;
 fun string_of_atom (t as Const (\<^const_name>\<open>numeral\<close>, _) $ _) = to_string t
   | string_of_atom (t as Const (\<^const_name>\<open>one_class.one\<close>, _)) = to_string t
   | string_of_atom (t as Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = to_string t