1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Thu Jul 28 11:43:27 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Sat Jul 30 16:47:45 2022 +0200
     1.3 @@ -480,7 +480,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.steps_reverse thy eval_rls rules ro NONE t';
     1.8 +    val der = Derive.steps_reverse (Proof_Context.init_global thy) eval_rls rules ro NONE t';
     1.9      val der = der @ 
    1.10        [(\<^rule_thm>\<open>real_mult_div_cancel2\<close>, (t'', asm))]
    1.11      val rs = (Rule.distinct' o (map #1)) der
    1.12 @@ -491,7 +491,7 @@
    1.13  fun locate_rule thy eval_rls ro [rs] t r =
    1.14      if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
    1.15      then 
    1.16 -      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Rule.thm r) t;
    1.17 +      let val ropt = Rewrite.rewrite_ (Proof_Context.init_global thy) ro eval_rls true (Rule.thm r) t;
    1.18        in
    1.19          case ropt of SOME ta => [(r, ta)]
    1.20  	      | NONE => ((*tracing 
    1.21 @@ -502,7 +502,7 @@
    1.22  
    1.23  fun next_rule thy eval_rls ro [rs] t =
    1.24      let
    1.25 -      val der = Derive.do_one thy eval_rls rs ro NONE t;
    1.26 +      val der = Derive.do_one (Proof_Context.init_global thy) eval_rls rs ro NONE t;
    1.27      in case der of (_, r, _) :: _ => SOME r | _ => NONE end
    1.28    | next_rule _ _ _ _ _ = raise ERROR ("next_rule: doesnt match rev-sets in istate");
    1.29  
    1.30 @@ -541,7 +541,7 @@
    1.31    let 
    1.32      val SOME (t', _) = common_nominator_p_ thy t;
    1.33      val SOME (t'', asm) = add_fraction_p_ thy t;
    1.34 -    val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
    1.35 +    val der = Derive.steps_reverse (Proof_Context.init_global thy) eval_rls rules ro NONE t';
    1.36      val der = der @ 
    1.37        [(\<^rule_thm>\<open>real_mult_div_cancel2\<close>, (t'',asm))]
    1.38      val rs = (Rule.distinct' o (map #1)) der;
    1.39 @@ -552,7 +552,7 @@
    1.40  fun locate_rule thy eval_rls ro [rs] t r =
    1.41      if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
    1.42      then 
    1.43 -      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Rule.thm r) t;
    1.44 +      let val ropt = Rewrite.rewrite_ (Proof_Context.init_global thy) ro eval_rls true (Rule.thm r) t;
    1.45        in 
    1.46          case ropt of
    1.47            SOME ta => [(r, ta)]
    1.48 @@ -563,7 +563,7 @@
    1.49    | locate_rule _ _ _ _ _ _ = raise ERROR "locate_rule: doesnt match rev-sets in istate";
    1.50  
    1.51  fun next_rule thy eval_rls ro [rs] t =
    1.52 -    let val der = Derive.do_one thy eval_rls rs ro NONE t;
    1.53 +    let val der = Derive.do_one (Proof_Context.init_global thy) eval_rls rs ro NONE t;
    1.54      in 
    1.55        case der of
    1.56  	      (_,r,_)::_ => SOME r