1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon Apr 27 16:40:11 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Tue Apr 28 15:31:49 2020 +0200
     1.3 @@ -479,8 +479,8 @@
     1.4      val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
     1.5      val der = der @ 
     1.6        [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'', asm))]
     1.7 -    val rs = (Rtools.distinct_Thm o (map #1)) der
     1.8 -  	val rs = filter_out (Rtools.eq_Thms 
     1.9 +    val rs = (Rule.distinct o (map #1)) der
    1.10 +  	val rs = filter_out (ThmC.member 
    1.11    	  ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs
    1.12    in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;
    1.13  
    1.14 @@ -540,8 +540,8 @@
    1.15      val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
    1.16      val der = der @ 
    1.17        [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'',asm))]
    1.18 -    val rs = (Rtools.distinct_Thm o (map #1)) der;
    1.19 -    val rs = filter_out (Rtools.eq_Thms 
    1.20 +    val rs = (Rule.distinct o (map #1)) der;
    1.21 +    val rs = filter_out (ThmC.member 
    1.22        ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs;
    1.23    in (t, t'', [rs(*here only _ONE_*)], der) end;
    1.24