1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Thu Apr 23 09:29:56 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Thu Apr 23 12:34:54 2020 +0200
     1.3 @@ -476,7 +476,7 @@
     1.4    let
     1.5      val SOME (t', _) = factout_p_ thy t;
     1.6      val SOME (t'', asm) = cancel_p_ thy t;
     1.7 -    val der = Derive.reverse_deriv thy eval_rls rules ro NONE t';
     1.8 +    val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
     1.9      val der = der @ 
    1.10        [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'', asm))]
    1.11      val rs = (Rtools.distinct_Thm o (map #1)) der
    1.12 @@ -498,7 +498,7 @@
    1.13  
    1.14  fun next_rule thy eval_rls ro [rs] t =
    1.15      let
    1.16 -      val der = Derive.make_deriv thy eval_rls rs ro NONE t;
    1.17 +      val der = Derive.do_one thy eval_rls rs ro NONE t;
    1.18      in case der of (_, r, _) :: _ => SOME r | _ => NONE end
    1.19    | next_rule _ _ _ _ _ = error ("next_rule: doesnt match rev-sets in istate");
    1.20  
    1.21 @@ -537,7 +537,7 @@
    1.22    let 
    1.23      val SOME (t',_) = common_nominator_p_ thy t;
    1.24      val SOME (t'', asm) = add_fraction_p_ thy t;
    1.25 -    val der = Derive.reverse_deriv thy eval_rls rules ro NONE t';
    1.26 +    val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
    1.27      val der = der @ 
    1.28        [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'',asm))]
    1.29      val rs = (Rtools.distinct_Thm o (map #1)) der;
    1.30 @@ -559,7 +559,7 @@
    1.31    | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
    1.32  
    1.33  fun next_rule thy eval_rls ro [rs] t =
    1.34 -    let val der = Derive.make_deriv thy eval_rls rs ro NONE t;
    1.35 +    let val der = Derive.do_one thy eval_rls rs ro NONE t;
    1.36      in 
    1.37        case der of
    1.38  	      (_,r,_)::_ => SOME r