1.1 --- a/src/Tools/isac/Interpret/generate.sml	Wed Apr 06 18:01:02 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Thu Apr 07 16:31:05 2011 +0200
     1.3 @@ -409,11 +409,10 @@
     1.4    let val (pt,c) = cappend_form pt p l f 
     1.5        val pt = update_branch pt p TransitiveB (*040312*)
     1.6  
     1.7 -      val ctxt = e_ctxt;
     1.8        val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f 
     1.9 -      val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt)
    1.10 +      val tac_ = Apply_Method' (e_metID, SOME t, is, e_ctxt)
    1.11        val pos' = ((lev_on o lev_dn) p, Frm)
    1.12 -  in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
    1.13 +  in (*implicit Take*) generate1 thy tac_ (is, e_ctxt) pos' pt end
    1.14  
    1.15    | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt =
    1.16    let (*val _= tracing("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*)
    1.17 @@ -428,11 +427,10 @@
    1.18    let val (pt,c) = cappend_form pt p l f 
    1.19        val pt = update_branch pt p TransitiveB (*040312*)
    1.20  
    1.21 -      val ctxt = e_ctxt;
    1.22        val is = init_istate (Rewrite_Set (id_rls rls)) f
    1.23 -      val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt)
    1.24 +      val tac_ = Apply_Method' (e_metID, SOME t, is, e_ctxt)
    1.25        val pos' = ((lev_on o lev_dn) p, Frm)
    1.26 -  in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
    1.27 +  in (*implicit Take*) generate1 thy tac_ (is, e_ctxt) pos' pt end
    1.28  
    1.29    | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
    1.30      let (*val _=tracing("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*)
    1.31 @@ -487,6 +485,7 @@
    1.32      error ("generate1: not impl.for "^(tac_2str m'))
    1.33  ;
    1.34  
    1.35 +
    1.36  fun generate_hard thy m' (p,p_) pt =
    1.37    let  
    1.38      val p = case p_ of Frm => p | Res => lev_on p