1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Fri Aug 05 11:41:06 2022 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Fri Aug 05 12:30:16 2022 +0200
     1.3 @@ -519,7 +519,7 @@
     1.4            | Rule.Eval (cc as (op_, _)) => 
     1.5              let val _= trace1 i (" try calc: " ^ op_ ^ "'")
     1.6                val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
     1.7 -            in case Eval.adhoc_thm thy 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 @@ -533,7 +533,7 @@
    1.13            | Rule.Cal1 (cc as (op_, _)) => 
    1.14              let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
    1.15                val ct = TermC.uminus_to_string ct
    1.16 -            in case Eval.adhoc_thm1_ thy cc ct of
    1.17 +            in case Eval.adhoc_thm1_ @{context} cc ct of
    1.18                  NONE => (ct, asm)
    1.19                | SOME (_, thm') =>
    1.20                  let