1.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml	Thu Oct 27 09:53:54 2016 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml	Thu Oct 27 10:48:10 2016 +0200
     1.3 @@ -36,10 +36,10 @@
     1.4  val SOME (t,_) = rewrite_inst_ thy e_rew_ord e_rls true subst 
     1.5    (num_str @{thm "int_isolate_add"}) t; term2str t;
     1.6  
     1.7 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; 
     1.8 +val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES"))) t; 
     1.9  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
    1.10  
    1.11 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; 
    1.12 +val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t; 
    1.13  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
    1.14  
    1.15  "----------- mathengine with usecase1 -------------------";
    1.16 @@ -71,10 +71,10 @@
    1.17        SOME t' => t'
    1.18      | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2";
    1.19  
    1.20 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; 
    1.21 +val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES"))) t; 
    1.22  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
    1.23  
    1.24 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; 
    1.25 +val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t; 
    1.26  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
    1.27  
    1.28