1.1 --- a/src/Tools/isac/Interpret/derive.sml	Sat Aug 06 18:50:43 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/derive.sml	Sat Aug 06 19:05:33 2022 +0200
     1.3 @@ -121,8 +121,8 @@
     1.4      fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
     1.5        | derivat dt = (#1 o #3 o last_elem) dt
     1.6      fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
     1.7 -    val  fod = do_one (** )ctxt( *HACK*)(Proof_Context.init_global (ThyC.Isac()))(**) erls rules (snd rew_ord) NONE  fo
     1.8 -    val ifod = do_one (** )ctxt( *HACK*)(Proof_Context.init_global (ThyC.Isac()))(**) erls rules (snd rew_ord) NONE ifo
     1.9 +    val  fod = do_one (** )ctxt( *HACK*)(Proof_Context.init_global (ThyC.Isac()))(*ctxt*) erls rules (snd rew_ord) NONE  fo
    1.10 +    val ifod = do_one (** )ctxt( *HACK*)(Proof_Context.init_global (ThyC.Isac()))(*ctxt*) erls rules (snd rew_ord) NONE ifo
    1.11    in 
    1.12      case (fod, ifod) of
    1.13        ([], []) => if fo = ifo then (true, []) else (false, [])

     2.1 --- a/src/Tools/isac/MathEngine/fetch-tactics.sml	Sat Aug 06 18:50:43 2022 +0200
     2.2 +++ b/src/Tools/isac/MathEngine/fetch-tactics.sml	Sat Aug 06 19:05:33 2022 +0200
     2.3 @@ -49,8 +49,13 @@
     2.4      else
     2.5        let
     2.6          val pp = par_pblobj pt p
     2.7 +(*ctxt* )
     2.8          val thy' = get_obj g_domID pt pp
     2.9          val thy = ThyC.get_theory thy'
    2.10 +( **)
    2.11 +val ctxt = Ctree.get_loc pt pos |> snd
    2.12 +val thy = Proof_Context.theory_of ctxt
    2.13 +(**)
    2.14          val metID = get_obj g_metID pt pp
    2.15          val metID' =
    2.16            if metID = MethodC.id_empty