1.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Mon Apr 06 11:44:36 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Wed Apr 08 12:32:51 2020 +0200
1.3 @@ -33,7 +33,7 @@
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 e_rls true subst
1.8 +val SOME (t,_) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst
1.9 (num_str @{thm "int_isolate_add"}) t; term2str t;
1.10
1.11 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;