1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Tue Apr 14 12:39:26 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Tue Apr 14 15:56:15 2020 +0200
     1.3 @@ -52,12 +52,12 @@
     1.4      let fun selc var = 
     1.5  	    case (Symbol.explode o id_of) var of
     1.6  		"c"::[] => true
     1.7 -	      |	"c"::"_"::is => (case (TermC.int_of_str_opt o implode) is of
     1.8 +	      |	"c"::"_"::is => (case (TermC.int_opt_of_string o implode) is of
     1.9  				     SOME _ => true
    1.10  				   | NONE => false)
    1.11                | _ => false;
    1.12  	fun get_coeff c = case (Symbol.explode o id_of) c of
    1.13 -	      		      "c"::"_"::is => (the o TermC.int_of_str_opt o implode) is
    1.14 +	      		      "c"::"_"::is => (the o TermC.int_opt_of_string o implode) is
    1.15  			    | _ => 0;
    1.16          val cs = filter selc (TermC.vars term);
    1.17      in