1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Fri Aug 05 11:41:06 2022 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Fri Aug 05 12:30:16 2022 +0200
     1.3 @@ -173,7 +173,7 @@
     1.4                  (* once again try the same rule, e.g. associativity against "()"*)
     1.5            | Rule.Eval (cc as (op_, _)) =>
     1.6              let val _ = trace_in1 ctxt i "try calc" op_;
     1.7 -            in case Eval.adhoc_thm (Proof_Context.theory_of ctxt) cc ct of
     1.8 +            in case Eval.adhoc_thm ctxt cc ct of
     1.9                  NONE => rew_once ruls asm ct apno thms
    1.10                | SOME (_, thm') => 
    1.11                  let 
    1.12 @@ -185,7 +185,7 @@
    1.13              end
    1.14            | Rule.Cal1 (cc as (op_, _)) => 
    1.15              let val _ = trace_in1 ctxt i "try cal1" op_;
    1.16 -            in case Eval.adhoc_thm1_ (Proof_Context.theory_of ctxt) cc ct of
    1.17 +            in case Eval.adhoc_thm1_ ctxt cc ct of
    1.18                  NONE => (ct, asm)
    1.19                | SOME (_, thm') =>
    1.20                  let 
    1.21 @@ -205,7 +205,6 @@
    1.22        val _ = trace_eq1 ctxt i "rls" rls ct
    1.23        val (ct', asm') = rew_once ruls [] ct Noap ruls;
    1.24  	  in if ct = ct' then NONE else SOME (ct', distinct op =  asm') end
    1.25 -(*--vvv and app_sub are type correct-----------------------------------------------------------*)
    1.26  and app_rev ctxt i rrls t =             (* apply an Rrls; if not applicable proceed with subterms*)
    1.27    let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
    1.28      fun chk_prepat _ _ [] _ = true
    1.29 @@ -284,7 +283,7 @@
    1.30  
    1.31  (* search ct for adjacent numerals and calculate them by operator isa_fn *)
    1.32  fun calculate_ ctxt (isa_fn as (id, eval_fn)) t =
    1.33 -  case Eval.adhoc_thm (Proof_Context.theory_of ctxt) isa_fn t of
    1.34 +  case Eval.adhoc_thm ctxt isa_fn t of
    1.35  	  NONE => NONE
    1.36  	| SOME (thmID, thm) =>
    1.37  	  (let val rew = case rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm t of