1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Tue Apr 14 12:39:26 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Tue Apr 14 15:56:15 2020 +0200
     1.3 @@ -125,10 +125,10 @@
     1.4      (c, list_update es (find_index (curry op = t) vs) 1)
     1.5    | monom_of_term  vs (c, es) (t as Free (id, _)) =
     1.6      if TermC.is_num' id 
     1.7 -    then (id |> TermC.int_of_str_opt |> the |> curry op * c, es) (*several numerals in one monom*)
     1.8 +    then (id |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
     1.9      else (c, list_update es (find_index (curry op = t) vs) 1)
    1.10    | monom_of_term  vs (c, es) (Const ("Prog_Expr.pow", _) $ (t as Free _) $ Free (e, _)) =
    1.11 -    (c, list_update es (find_index (curry op = t) vs) (the (TermC.int_of_str_opt e)))
    1.12 +    (c, list_update es (find_index (curry op = t) vs) (the (TermC.int_opt_of_string e)))
    1.13    | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
    1.14      let val (c', es') = monom_of_term vs (c, es) m1
    1.15      in monom_of_term vs (c', es') m2 end