diff -r 638d02a9a96a -r e6e7a9b9ced7 src/Tools/isac/ProgLang/Prog_Expr.thy
--- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Tue Jun 01 15:41:23 2021 +0200
+++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Sat Jul 03 16:21:07 2021 +0200
@@ -290,32 +290,35 @@
 
 fun even i = (i div 2) * 2 = i;
 (*("is_even",("Prog_Expr.is_even", eval_is_even "#is_even_"))*)
-fun eval_is_even (thmid:string) "Prog_Expr.is_even"
-		 (t as (Const _ $ arg)) _ = 
-    (case arg of 
-	Free (n,_) =>
-	 (case ThmC_Def.int_opt_of_string n of
-	      SOME i =>
-	      if even i then SOME (TermC.mk_thmid thmid n "", 
-				   HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
+fun eval_is_even (thmid:string) "Prog_Expr.is_even" (t as (Const _ $ arg)) _ = 
+    if TermC.is_num arg
+    then
+      let
+        val i = arg |> HOLogic.dest_number |> snd
+      in
+	      if even i 
+        then SOME (TermC.mk_thmid thmid (string_of_int i) "", 
+				  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
 	      else SOME (TermC.mk_thmid thmid "" "", 
-			 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
-	    | _ => NONE)
-       | _ => NONE)
+			    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
+      end
+    else NONE
   | eval_is_even _ _ _ _ = NONE; 
 
-(*evaluate 'is_const'*)
 (*("is_const",("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"))*)
-fun eval_const (thmid:string) _ (t as (Const _ $ arg)) _ = 
-    (case arg of 
-       Const (n1, _) =>
-	     SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
-     | n1 =>
-	     if TermC.is_num n1
-	     then SOME (TermC.mk_thmid thmid (TermC.string_of_num n1) "",
-         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
-	     else SOME (TermC.mk_thmid thmid (UnparseC.term n1) "",
-         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
+fun eval_const thmid _ (t as (Const ("Prog_Expr.is_const", _) $ Const ("Partial_Fractions.AA", _))) _ =
+    (*TODO get rid of this special case*)
+    SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
+      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
+  | eval_const thmid _ (t as (Const ("Prog_Expr.is_const", _) $ Const _)) _ =
+    SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
+      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
+  | eval_const thmid _ (t as (Const ("Prog_Expr.is_const", _) $ n)) _ =
+	   if TermC.is_num n
+	   then SOME (TermC.mk_thmid thmid (TermC.string_of_num n) "",
+       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
+	   else SOME (TermC.mk_thmid thmid (UnparseC.term n) "",
+       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
   | eval_const _ _ _ _ = NONE; 
 
 (*. evaluate binary, associative, commutative operators: *,+,^ .*)