1.1 --- a/src/Tools/isac/Knowledge/RootRat.thy	Mon Apr 06 11:44:36 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy	Wed Apr 08 12:32:51 2020 +0200
     1.3 @@ -9,13 +9,13 @@
     1.4  val thy = @{theory};
     1.5  
     1.6  val rootrat_erls = 
     1.7 -  Rule_Set.merge_rls "rootrat_erls" Root_erls
     1.8 -    (Rule_Set.merge_rls "" rational_erls
     1.9 -      (Rule_Set.append_rls "" Rule_Set.e_rls []));
    1.10 +  Rule_Set.merge "rootrat_erls" Root_erls
    1.11 +    (Rule_Set.merge "" rational_erls
    1.12 +      (Rule_Set.append_rules "" Rule_Set.empty []));
    1.13  
    1.14  (*.calculate numeral groundterms.*)
    1.15  val calculate_RootRat = 
    1.16 -  Rule_Set.append_rls "calculate_RootRat" calculate_Rational
    1.17 +  Rule_Set.append_rules "calculate_RootRat" calculate_Rational
    1.18  	    [Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
    1.19  		      (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
    1.20  		     Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),