diff -r 820bf0840029 -r 995177b6d786 src/Tools/isac/ProgLang/Prog_Expr.thy
--- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Tue Apr 14 12:39:26 2020 +0200
+++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Tue Apr 14 15:56:15 2020 +0200
@@ -300,7 +300,7 @@
 		 (t as (Const _ $ arg)) _ = 
     (case arg of 
 	Free (n,_) =>
-	 (case ThmC_Def.int_of_str_opt n of
+	 (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})))
@@ -344,7 +344,7 @@
   ("leq"     ,("Orderings.ord_class.less_eq"       , Prog_Expr.eval_equ "#less_equal_"))*)
 fun eval_equ (thmid:string) (_(*op_*)) (t as 
 	       (Const (op0, _) $ Free (n1, _) $ Free(n2, _))) _ = 
-    (case (ThmC_Def.int_of_str_opt n1, ThmC_Def.int_of_str_opt n2) of
+    (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
 	 (SOME n1', SOME n2') =>
   if Num_Calc.calc_equ (strip_thy op0) (n1', n2')
     then SOME (TermC.mk_thmid thmid n1 n2, 
@@ -437,7 +437,7 @@
 (*("DIVIDE" ,("Rings.divide_class.divide"  , eval_cancel "#divide_e"))*)
 fun eval_cancel (thmid: string) "Rings.divide_class.divide" (t as 
 	       (Const (op0,t0) $ Free (n1, _) $ Free(n2, _))) _ = 
-    (case (ThmC_Def.int_of_str_opt n1, ThmC_Def.int_of_str_opt n2) of
+    (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
     	(SOME n1', SOME n2') =>
         let 
           val sg = Num_Calc.sign_mult n1' n2';