diff -r 820bf0840029 -r 995177b6d786 src/Tools/isac/Knowledge/Integrate.thy
--- a/src/Tools/isac/Knowledge/Integrate.thy	Tue Apr 14 12:39:26 2020 +0200
+++ b/src/Tools/isac/Knowledge/Integrate.thy	Tue Apr 14 15:56:15 2020 +0200
@@ -52,12 +52,12 @@
     let fun selc var = 
 	    case (Symbol.explode o id_of) var of
 		"c"::[] => true
-	      |	"c"::"_"::is => (case (TermC.int_of_str_opt o implode) is of
+	      |	"c"::"_"::is => (case (TermC.int_opt_of_string o implode) is of
 				     SOME _ => true
 				   | NONE => false)
               | _ => false;
 	fun get_coeff c = case (Symbol.explode o id_of) c of
-	      		      "c"::"_"::is => (the o TermC.int_of_str_opt o implode) is
+	      		      "c"::"_"::is => (the o TermC.int_opt_of_string o implode) is
 			    | _ => 0;
         val cs = filter selc (TermC.vars term);
     in