1.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Mon Jul 19 17:29:35 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Mon Jul 19 18:29:46 2021 +0200
1.3 @@ -34,7 +34,7 @@
1.4 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";
1.5
1.6 val SOME (t,_) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst
1.7 - (ThmC.numerals_to_Free @{thm "int_isolate_add"}) t; UnparseC.term t;
1.8 + @{thm "int_isolate_add"} t; UnparseC.term t;
1.9
1.10 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
1.11 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; UnparseC.term t;