1.1 --- a/src/Tools/isac/Knowledge/RootRat.thy	Mon Apr 13 13:27:55 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy	Mon Apr 13 15:31:23 2020 +0200
     1.3 @@ -16,11 +16,11 @@
     1.4  (*.calculate numeral groundterms.*)
     1.5  val calculate_RootRat = 
     1.6    Rule_Set.append_rules "calculate_RootRat" calculate_Rational
     1.7 -	    [Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
     1.8 +	    [Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
     1.9  		      (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
    1.10 -		     Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
    1.11 +		     Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
    1.12  		      (* 1 * z = z *)
    1.13 -		     Rule.Thm ("sym_real_mult_minus1",TermC.num_str (@{thm real_mult_minus1} RS @{thm sym})),
    1.14 +		     Rule.Thm ("sym_real_mult_minus1",ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})),
    1.15  		       (* "- z1 = -1 * z1"  *)
    1.16  		     Rule.Num_Calc ("NthRoot.sqrt", eval_sqrt "#sqrt_")
    1.17  		     ];