1.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Thu Jul 28 11:43:27 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Sat Jul 30 16:47:45 2022 +0200
1.3 @@ -33,14 +33,14 @@
1.4 SOME t' => t'
1.5 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";
1.6
1.7 -val SOME (t,_) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst
1.8 +val SOME (t,_) = rewrite_inst_ ctxt e_rew_ord Rule_Set.empty true subst
1.9 @{thm "int_isolate_add"} t; UnparseC.term t;
1.10
1.11 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
1.12 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; UnparseC.term t;
1.13 +val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
1.14
1.15 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
1.16 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; UnparseC.term t;
1.17 +val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
1.18
1.19 "----------- mathengine with usecase1 -------------------";
1.20 "----------- mathengine with usecase1 -------------------";
1.21 @@ -72,10 +72,10 @@
1.22 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2";
1.23
1.24 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
1.25 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; UnparseC.term t;
1.26 +val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
1.27
1.28 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
1.29 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; UnparseC.term t;
1.30 +val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
1.31
1.32
1.33 "----------- mathengine with usecase2 -------------------";