1.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Wed Oct 30 14:40:22 2019 +0100
     1.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Wed Oct 30 16:46:05 2019 +0100
     1.3 @@ -47,8 +47,8 @@
     1.4          val thy' = get_obj g_domID pt p;
     1.5          val thy = assoc_thy thy';
     1.6          val srls = Lucin.get_simplifier (pt, pos)
     1.7 -        val (is as Istate.Pstate (env,_,_,_,_,_,_), ctxt, sc) = init_pstate srls ctxt itms mI;
     1.8 -        val ini = init_form thy sc env;
     1.9 +        val (is as Istate.Pstate ist, ctxt, sc) = init_pstate srls ctxt itms mI;
    1.10 +        val ini = init_form thy sc (Istate.get_env ist);
    1.11          val p = lev_dn p;
    1.12  ini = NONE; (*true*)
    1.13              val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);