diff -r 03151cfbdc02 -r 703d656a6291 src/Tools/isac/Interpret/generate.sml
--- a/src/Tools/isac/Interpret/generate.sml	Fri Apr 15 15:58:52 2011 +0200
+++ b/src/Tools/isac/Interpret/generate.sml	Fri Apr 15 17:07:34 2011 +0200
@@ -373,18 +373,21 @@
   in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)),
       pt) end
 
-  | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) l (p,p_) pt =
+  | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) (is, ctxt)
+      (p,p_) pt =
   let (*val _= tracing("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));*)
-      val (pt,c) = cappend_atomic pt p l f
+      val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
       (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete;
       val pt = update_branch pt p TransitiveB (*040312*)
     (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
   in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
       pt) end
 
-  | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) l (p,p_) pt =
+  | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) (is, ctxt)
+      (p,p_) pt =
   let (*val _= tracing("###generate1 Rewrite': pos= "^pos'2str (p,p_))*)
-      val (pt,c) = cappend_atomic pt p l f (Rewrite thm') (f',asm) Complete
+      val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
+        (Rewrite thm') (f',asm) Complete
       val pt = update_branch pt p TransitiveB (*040312*)
     (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
   in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
@@ -393,44 +396,46 @@
   | generate1 thy (Rewrite_Asm' all) l p pt = 
     generate1 thy (Rewrite' all) l p pt
 
-  | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) l (p,p_) pt =
+  | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) (is, ctxt)
+      (p,p_) pt =
 (* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) = 
        (assoc_thy "Isac", tac_, is, pos, pt);
    *)
   let (*val _=tracing("###generate1 Rewrite_Set_Inst': pos= "^pos'2str(p,p_))*)
-      val (pt,c) = cappend_atomic pt p l f 
+      val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f 
       (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete
       val pt = update_branch pt p TransitiveB (*040312*)
     (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
   in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
       pt) end
 
-  | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) l (p,p_) pt =
-  let val (pt,c) = cappend_form pt p l f 
+  | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) (is, ctxt) (p,p_)
+      pt =
+  let val ctxt' = insert_assumptions asm ctxt
+      val (pt,c) = cappend_form pt p (is, ctxt') f 
       val pt = update_branch pt p TransitiveB (*040312*)
+      val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f 
+      val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
+      val pos' = ((lev_on o lev_dn) p, Frm)
+  in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end
 
-      val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f 
-      val tac_ = Apply_Method' (e_metID, SOME t, is, e_ctxt)
-      val pos' = ((lev_on o lev_dn) p, Frm)
-  in (*implicit Take*) generate1 thy tac_ (is, e_ctxt) pos' pt end
-
-  | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt =
+  | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) (is, ctxt) (p,p_) pt =
   let (*val _= tracing("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*)
-      val (pt,c) = cappend_atomic pt p l f 
+      val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f 
       (Rewrite_Set (id_rls rls')) (f',asm) Complete
       val pt = update_branch pt p TransitiveB (*040312*)
     (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
   in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
       pt) end
 
-  | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) l (p,p_) pt =
-  let val (pt,c) = cappend_form pt p l f 
+  | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) (is, ctxt) (p,p_) pt =
+  let val (pt,c) = cappend_form pt p (is, ctxt) f 
       val pt = update_branch pt p TransitiveB (*040312*)
 
       val is = init_istate (Rewrite_Set (id_rls rls)) f
-      val tac_ = Apply_Method' (e_metID, SOME t, is, e_ctxt)
+      val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt)
       val pos' = ((lev_on o lev_dn) p, Frm)
-  in (*implicit Take*) generate1 thy tac_ (is, e_ctxt) pos' pt end
+  in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
 
   | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
     let (*val _=tracing("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*)
@@ -552,7 +557,7 @@
 	val (SOME (ist, ctxt),_) = get_obj g_loc pt p
 	val form = get_obj g_form pt p
       (*val p = lev_on p; ---------------only difference to (..,Res) below*)
-	val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, e_ctxt)))
+	val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt)))
 		    ::(insert_pos ((lev_on o lev_dn) p) tacis)
 		    @ [(End_Trans, End_Trans' (res, asm),
 			(pos_plus (length tacis) (lev_dn p, Res), 
@@ -573,7 +578,7 @@
 	val (_, SOME (ist, ctxt)) = get_obj g_loc pt p
 	val (f,a) = get_obj g_result pt p
 	val p = lev_on p(*---------------only difference to (..,Frm) above*);
-	val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, e_ctxt)))
+	val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt)))
 		    ::(insert_pos ((lev_on o lev_dn) p) tacis)
 		    @ [(End_Trans, End_Trans' (res, asm), 
 			(pos_plus (length tacis) (lev_dn p, Res),