1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Sat Aug 24 13:16:17 2019 +0200
     1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Mon Aug 26 09:20:07 2019 +0200
     1.3 @@ -582,7 +582,7 @@
     1.4                let
     1.5                  val (po, p_) = pos
     1.6                  val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_input_tactic " ^ pos_2str p_)
     1.7 -                val (p'',_,_,pt'') = Generate.generate1 thy tac' (Istate.Pstate is, ctxt) (po', p_) pt
     1.8 +                val (p'',_,_,pt'') = Generate.generate1 @{theory} tac' (Istate.Pstate is, ctxt) (po', p_) pt
     1.9   	             in
    1.10                   Unsafe_Step ((pt'',p''), Istate.Pstate is, get_ctxt ctree pos', tac')
    1.11                end