1.1 --- a/src/Tools/isac/Specify/specify.sml	Sat Feb 04 17:00:25 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/specify.sml	Tue Feb 07 17:25:09 2023 +0100
     1.3 @@ -91,10 +91,10 @@
     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_PIDE ctxt
     1.8 +          ("dummy", (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory 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 +        (case item_to_add (ThyC.get_theory ctxt
    1.13              (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
    1.14             SOME (fd, ct') => ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))
    1.15           | NONE => (*pbl-items complete*)        
    1.16 @@ -105,9 +105,9 @@
    1.17             else
    1.18              case find_first (I_Model.is_error o #5) met of
    1.19                SOME (_, _, _, fd, itm_) =>
    1.20 -                 ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory_PIDE ctxt dI) fd itm_))
    1.21 +                 ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory ctxt dI) fd itm_))
    1.22              | NONE => 
    1.23 -              (case item_to_add (ThyC.get_theory_PIDE ctxt dI) oris mpc met of
    1.24 +              (case item_to_add (ThyC.get_theory ctxt dI) oris mpc met of
    1.25      	          SOME (fd, ct') =>
    1.26                     ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*30.8.01: where_?!?*)
    1.27      		      | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI))))
    1.28 @@ -121,10 +121,10 @@
    1.29    in
    1.30      (case find_first (I_Model.is_error o #5) met of
    1.31        SOME (_,_,_, fd, itm_) =>
    1.32 -        ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory_PIDE ctxt
    1.33 +        ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory ctxt
    1.34              (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
    1.35      | NONE => 
    1.36 -      case item_to_add (ThyC.get_theory_PIDE ctxt 
    1.37 +      case item_to_add (ThyC.get_theory ctxt 
    1.38            (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
    1.39          SOME (fd, ct') =>
    1.40            ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*->->*)