diff -r 0d84c462dd7e -r 383722bfcff5 test/Tools/isac/Knowledge/diophanteq.sml
--- a/test/Tools/isac/Knowledge/diophanteq.sml	Thu Oct 27 09:53:54 2016 +0200
+++ b/test/Tools/isac/Knowledge/diophanteq.sml	Thu Oct 27 10:48:10 2016 +0200
@@ -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) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; 
+val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES"))) t; 
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
 
-val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; 
+val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"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) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; 
+val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES"))) t; 
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
 
-val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; 
+val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t; 
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;