1.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml Mon Apr 13 13:27:55 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml Mon Apr 13 15:31:23 2020 +0200
1.3 @@ -287,14 +287,14 @@
1.4
1.5 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*)
1.6 t |> UnparseC.term; t |> atomty;
1.7 -val thm = num_str @{thm d2_prescind1};
1.8 +val thm = ThmC.numerals_to_Free @{thm d2_prescind1};
1.9 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> atomty;
1.10 val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
1.11
1.12 (*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1",""))
1.13 --> x = 0 | -6 + 5 * x = 0*)
1.14 t' |> UnparseC.term; t' |> atomty;
1.15 -val thm = num_str @{thm d2_reduce_equation1};
1.16 +val thm = ThmC.numerals_to_Free @{thm d2_reduce_equation1};
1.17 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> atomty;
1.18 val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
1.19 (* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"