1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Tue Jun 21 13:51:04 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Tue Jun 21 16:04:43 2022 +0200
     1.3 @@ -96,7 +96,7 @@
     1.4            Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
     1.5          | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
     1.6          val {where_, ...} = Problem.from_store pI
     1.7 -        val pres = map (I_Model.mk_env probl |> subst_atomic) where_
     1.8 +        val pres = map (I_Model.environment probl |> subst_atomic) where_
     1.9          val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
    1.10            then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
    1.11            else ctxt