1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Sat Jun 12 18:06:27 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Sat Jun 12 18:22:07 2021 +0200
     1.3 @@ -439,9 +439,7 @@
     1.4         erls = PolyEq_erls,
     1.5         srls = Rule_Set.Empty, 
     1.6         calc = [], errpatts = [],
     1.7 -       rules = [\<^rule_thm>\<open>d0_true\<close>,
     1.8 -		Rule.Thm("d0_false",ThmC.numerals_to_Free @{thm  d0_false})
     1.9 -		],
    1.10 +       rules = [\<^rule_thm>\<open>d0_true\<close>, \<^rule_thm>\<open>d0_false\<close>],
    1.11         scr = Rule.Empty_Prog
    1.12         });
    1.13  
    1.14 @@ -1305,8 +1303,7 @@
    1.15  		(*"?bdv / ?b = (1 / ?b) * ?bdv"*)
    1.16  		\<^rule_thm>\<open>separate_1_bdv_n\<close>,
    1.17  		(*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
    1.18 -		Rule.Thm ("add_divide_distrib", 
    1.19 -		     ThmC.numerals_to_Free @{thm add_divide_distrib})
    1.20 +		\<^rule_thm>\<open>add_divide_distrib\<close>
    1.21  		(*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
    1.22  		      WN051031 DOES NOT BELONG TO HERE*)
    1.23  		];