1.1 --- a/src/Tools/isac/Knowledge/RootRat.thy	Mon Jul 19 17:29:35 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy	Mon Jul 19 18:29:46 2021 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  		      (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
     1.5  		     \<^rule_thm>\<open>mult_1_left\<close>,
     1.6  		      (* 1 * z = z *)
     1.7 -		      Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym})),
     1.8 +		      Rule.Thm ("real_mult_minus1_sym",  (@{thm real_mult_minus1_sym})),
     1.9  	        (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)
    1.10  		     Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_")
    1.11  		     ];