1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon Jul 19 17:29:35 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Mon Jul 19 18:29:46 2021 +0200
     1.3 @@ -410,8 +410,8 @@
     1.4         [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"),
     1.5          Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
     1.6          Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
     1.7 -        Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
     1.8 -        Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})], 
     1.9 +        Rule.Thm ("not_true",  @{thm not_true}),
    1.10 +        Rule.Thm ("not_false",  @{thm not_false})], 
    1.11        scr = Rule.Empty_Prog});
    1.12  
    1.13  (* simplifies expressions with numerals;
    1.14 @@ -425,7 +425,7 @@
    1.15        rules = 
    1.16          [\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    1.17  
    1.18 -        Rule.Thm ("minus_divide_left", ThmC.numerals_to_Free (@{thm minus_divide_left} RS @{thm sym})),
    1.19 +        Rule.Thm ("minus_divide_left",  (@{thm minus_divide_left} RS @{thm sym})),
    1.20            (*SYM - ?x / ?y = - (?x / ?y)  may come from subst*)
    1.21          \<^rule_thm>\<open>rat_add\<close>,
    1.22            (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \