1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Tue Apr 14 12:39:26 2020 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Tue Apr 14 15:56:15 2020 +0200
     1.3 @@ -300,7 +300,7 @@
     1.4  		 (t as (Const _ $ arg)) _ = 
     1.5      (case arg of 
     1.6  	Free (n,_) =>
     1.7 -	 (case ThmC_Def.int_of_str_opt n of
     1.8 +	 (case ThmC_Def.int_opt_of_string n of
     1.9  	      SOME i =>
    1.10  	      if even i then SOME (TermC.mk_thmid thmid n "", 
    1.11  				   HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.12 @@ -344,7 +344,7 @@
    1.13    ("leq"     ,("Orderings.ord_class.less_eq"       , Prog_Expr.eval_equ "#less_equal_"))*)
    1.14  fun eval_equ (thmid:string) (_(*op_*)) (t as 
    1.15  	       (Const (op0, _) $ Free (n1, _) $ Free(n2, _))) _ = 
    1.16 -    (case (ThmC_Def.int_of_str_opt n1, ThmC_Def.int_of_str_opt n2) of
    1.17 +    (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
    1.18  	 (SOME n1', SOME n2') =>
    1.19    if Num_Calc.calc_equ (strip_thy op0) (n1', n2')
    1.20      then SOME (TermC.mk_thmid thmid n1 n2, 
    1.21 @@ -437,7 +437,7 @@
    1.22  (*("DIVIDE" ,("Rings.divide_class.divide"  , eval_cancel "#divide_e"))*)
    1.23  fun eval_cancel (thmid: string) "Rings.divide_class.divide" (t as 
    1.24  	       (Const (op0,t0) $ Free (n1, _) $ Free(n2, _))) _ = 
    1.25 -    (case (ThmC_Def.int_of_str_opt n1, ThmC_Def.int_of_str_opt n2) of
    1.26 +    (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
    1.27      	(SOME n1', SOME n2') =>
    1.28          let 
    1.29            val sg = Num_Calc.sign_mult n1' n2';