1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Wed Jun 03 09:56:24 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Wed Jun 03 11:25:19 2020 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    is'_expanded    :: "real => bool" ("_ is'_expanded")     (*RL->Poly.thy*)
     1.5    is'_ratpolyexp  :: "real => bool" ("_ is'_ratpolyexp") 
     1.6    get_denominator :: "real => real"
     1.7 -  get_numerator   :: "real => real"
     1.8 +  get_numerator   :: "real => real"           
     1.9  
    1.10  ML \<open>
    1.11  (*.the expression contains + - * ^ / only ?.*)
    1.12 @@ -479,8 +479,8 @@
    1.13      val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
    1.14      val der = der @ 
    1.15        [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'', asm))]
    1.16 -    val rs = (Rule.distinct o (map #1)) der
    1.17 -  	val rs = filter_out (ThmC.member 
    1.18 +    val rs = (Rule.distinct' o (map #1)) der
    1.19 +  	val rs = filter_out (ThmC.member'
    1.20    	  ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs
    1.21    in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;
    1.22  
    1.23 @@ -540,8 +540,8 @@
    1.24      val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
    1.25      val der = der @ 
    1.26        [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'',asm))]
    1.27 -    val rs = (Rule.distinct o (map #1)) der;
    1.28 -    val rs = filter_out (ThmC.member 
    1.29 +    val rs = (Rule.distinct' o (map #1)) der;
    1.30 +    val rs = filter_out (ThmC.member'
    1.31        ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs;
    1.32    in (t, t'', [rs(*here only _ONE_*)], der) end;
    1.33