1.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Mon Nov 04 11:40:29 2019 +0100
1.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Wed Nov 06 15:08:27 2019 +0100
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) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
1.8 +val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"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) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
1.12 +val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"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) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
1.21 +val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"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) = adhoc_thm thy (the(assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
1.25 +val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
1.26 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
1.27
1.28