1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Sat Jun 12 14:27:03 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Sat Jun 12 14:29:10 2021 +0200
     1.3 @@ -252,8 +252,7 @@
     1.4  	       (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
     1.5  	       Rule.Rls_ norm_Rational_noadd_fractions(**2**),
     1.6  	       Rule.Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**),
     1.7 -	       Rule.Thm ("sym_mult.assoc",
     1.8 -                     ThmC.numerals_to_Free (@{thm mult.assoc} RS @{thm sym}))
     1.9 +	       \<^rule_thm_sym>\<open>mult.assoc\<close>
    1.10  	       (*Rule.Rls_ discard_parentheses *3**),
    1.11  	       Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
    1.12  	       Rule.Rls_ separate_bdv2,
    1.13 @@ -281,8 +280,7 @@
    1.14  (*
    1.15  val simplify_System = 
    1.16      Rule_Set.append_rules "simplify_System" simplify_System_parenthesized
    1.17 -	       [Rule.Thm ("sym_add.assoc",
    1.18 -                      ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym}))];
    1.19 +	       [\<^rule_thm_sym>\<open>add.assoc\<close>];
    1.20  *)
    1.21  \<close>
    1.22  ML \<open>