1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Tue May 05 13:33:23 2020 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Tue May 05 15:39:20 2020 +0200
     1.3 @@ -99,7 +99,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_, ...} = Specify.get_pbt pI
     1.7 -        val pres = map (Model.mk_env probl |> subst_atomic) where_
     1.8 +        val pres = map (I_Model.mk_env 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