1.1 --- a/src/Tools/isac/Specify/step-specify.sml	Wed Nov 09 15:15:24 2022 +0100
     1.2 +++ b/src/Tools/isac/Specify/step-specify.sml	Thu Nov 10 14:25:38 2022 +0100
     1.3 @@ -88,16 +88,15 @@
     1.4      end
     1.5    | by_tactic_input (Tactic.Specify_Problem pI) (pt, pos as (p, _)) =
     1.6      let
     1.7 -      val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
     1.8 -        PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
     1.9 -          (oris, dI, dI', pI', probl, ctxt)
    1.10 +      val (oris, pI', probl, ctxt) = case get_obj I pt p of
    1.11 +        PblObj {origin = (oris, _, _), spec = (_ ,pI',_), probl, ctxt, ...} =>
    1.12 +          (oris, pI', probl, ctxt)
    1.13        | _ => raise ERROR ""
    1.14 -	    val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');
    1.15        val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
    1.16  	    val pbl = 
    1.17  	      if pI' = Problem.id_empty andalso pI = Problem.id_empty
    1.18  	      then (false, (I_Model.init model, []))
    1.19 -	      else M_Match.match_itms_oris thy probl (model, where_, where_rls) oris
    1.20 +	      else M_Match.match_itms_oris ctxt probl (model, where_, where_rls) oris
    1.21  	      (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
    1.22  	    val (c, pt) =
    1.23  	      case Specify_Step.add (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of