1.1 --- a/src/Tools/isac/Specify/specify.sml	Fri Jan 06 11:43:50 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/specify.sml	Fri Jan 06 15:06:40 2023 +0100
     1.3 @@ -91,7 +91,7 @@
     1.4      else
     1.5        case find_first (I_Model.is_error o #5) pbl of
     1.6          SOME (_, _, _, fd, itm_) =>
     1.7 -          ("dummy", (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory
     1.8 +          ("dummy", (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory_PIDE ctxt
     1.9              (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
    1.10        | NONE => 
    1.11          (case item_to_add (ThyC.get_theory_PIDE ctxt
    1.12 @@ -105,9 +105,9 @@
    1.13             else
    1.14              case find_first (I_Model.is_error o #5) met of
    1.15                SOME (_, _, _, fd, itm_) =>
    1.16 -                 ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_))
    1.17 +                 ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory_PIDE ctxt dI) fd itm_))
    1.18              | NONE => 
    1.19 -              (case item_to_add (ThyC.get_theory dI) oris mpc met of
    1.20 +              (case item_to_add (ThyC.get_theory_PIDE ctxt dI) oris mpc met of
    1.21      	          SOME (fd, ct') =>
    1.22                     ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*30.8.01: where_?!?*)
    1.23      		      | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI))))