diff -r 08512202c2c6 -r 3ce3d089bd64 test/Tools/isac/Knowledge/diophanteq.sml
--- a/test/Tools/isac/Knowledge/diophanteq.sml	Mon Nov 04 11:40:29 2019 +0100
+++ b/test/Tools/isac/Knowledge/diophanteq.sml	Wed Nov 06 15:08:27 2019 +0100
@@ -36,10 +36,10 @@
 val SOME (t,_) = rewrite_inst_ thy e_rew_ord e_rls true subst 
   (num_str @{thm "int_isolate_add"}) t; term2str t;
 
-val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; 
+val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; 
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
 
-val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; 
+val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; 
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
 
 "----------- mathengine with usecase1 -------------------";
@@ -71,10 +71,10 @@
       SOME t' => t'
     | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2";
 
-val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; 
+val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; 
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
 
-val SOME (thmID,thm) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; 
+val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; 
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;