(* use"ME/generate.sml";

   use"generate.sml";

   *)

(*.initialize istate for Detail_Set.*)

fun init_istate (Rewrite_Set rls) = 

    (case assoc_rls rls of

	 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t))

       | Rls {scr=Script s,...} =>

(* val Rls {scr=Script s,...} = assoc_rls rls;

   *)

	 (ScrState ([(one_scr_arg s, t)], [], None, e_term, Sundef, true))

       | Seq {srls=srls,scr=Script s,...} =>

	 (ScrState ([(one_scr_arg s, t)], [], None, e_term, Sundef, true)))

  | init_istate (Rewrite_Set_Inst (subs, rls)) =

    let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs

    in case assoc_rls rls of

	   Rls {scr=Script s,...} =>

	   let val (a1, a2) = two_scr_arg s

	   in (ScrState ([(a1, v), (a2, t)],[], None, e_term, Sundef,true)) end

	 | Seq {scr=Script s,...} =>

	   let val (a1, a2) = two_scr_arg s

	   in (ScrState ([(a1, v), (a2, t)],[], None, e_term, Sundef,true)) end

    end;

type taci = 

     (tac *            (*for comparison with input tac*)      

      tac_ *           (*for ptree generation*)

      (pos' *          (*after applying tac_, for ptree generation*)

       istate));       (*after applying tac_, for ptree generation*)

val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', e_istate)): taci;

(* val (tac, tac_, (pos', istate))::_ = tacis';

   *)

fun taci2str ((tac, tac_, (pos', istate)):taci) =

    "( "^tac2str tac^", "^tac_2str tac_^", ( "^pos'2str pos'

    ^", "^istate2str istate^" ))";

fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis;

datatype pblmet =       (*%^%*)

    Upblmet             (*undefined*)

  | Problem of pblID    (*%^%*)

  | Method of metID;    (*%^%*)

fun pblmet2str (Problem pblID) = "Problem "^(strs2str pblID)(*%^%*)

  | pblmet2str (Method metID) = "Method "^(metID2str metID);(*%^%*)

      (*%^%*)   (*26.6. moved to sequent.sml: fun ~~~~~~~~~; was here below*)

(* copy from 03.60.usecases.sml 15.11.99 *)

datatype user_cmd = 

  Accept   | NotAccept | Example

| YourTurn | MyTurn (* internal use only 7.6.02 java-sml*)   

| Rules

| DontKnow  (*| HowComes | WhatFor       7.6.02 java-sml*)

| Undo      (*| Back          | Forward  7.6.02 java-sml*)

| EndProof | EndSession

| ActivePlus | ActiveMinus | SpeedPlus | SpeedMinus

                           (*Stepwidth...7.6.02 java-sml*)

| Auto | NotAuto | Details;

(* for test-print-outs *)

fun user_cmd2str Accept     ="Accept"

  | user_cmd2str NotAccept  ="NotAccept"

  | user_cmd2str Example    ="Example"

  | user_cmd2str MyTurn     ="MyTurn"

  | user_cmd2str YourTurn   ="YourTurn"

  | user_cmd2str Rules	    ="Rules"

(*| user_cmd2str HowComes   ="HowComes"*)

  | user_cmd2str DontKnow   ="DontKnow"

(*| user_cmd2str WhatFor    ="WhatFor"

  | user_cmd2str Back       ="Back"*)

  | user_cmd2str Undo       ="Undo"

(*| user_cmd2str Forward    ="Forward"*)

  | user_cmd2str EndProof   ="EndProof"

  | user_cmd2str EndSession ="EndSession"

  | user_cmd2str ActivePlus = "ActivePlus"

  | user_cmd2str ActiveMinus = "ActiveMinus"

  | user_cmd2str SpeedPlus = "SpeedPlus"

  | user_cmd2str SpeedMinus = "SpeedMinus"

  | user_cmd2str Auto = "Auto"

  | user_cmd2str NotAuto = "NotAuto"

  | user_cmd2str Details = "Details";

(*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)

datatype foppFK =                  (* in DG cases div 2 *)

  EmptyFoppFK         (*DG internal*)

| FormFK of cterm'

| PpcFK of cterm' ppc;

fun foppFK2str (FormFK ct') ="FormFK "^ct'

  | foppFK2str (PpcFK  ppc) ="PpcFK "^(ppc2str ppc)

  | foppFK2str EmptyFoppFK  ="EmptyFoppFK";

datatype nest = Open | Closed | Nundef;

fun nest2str Open = "Open"

  | nest2str Closed = "Closed"

  | nest2str Nundef = "Nundef";

type indent = int;

datatype edit = EdUndef | Write | Protect;

                                   (* bridge --> kernel *)

                                   (* bridge <-> kernel *)

(* needed in dialog.sml *)         (* bridge <-- kernel *)

fun edit2str EdUndef = "EdUndef"

  | edit2str Write = "Write"

  | edit2str Protect = "Protect";

datatype inout =

  New_User | End_User                                          (*<->*)

| New_Proof | End_Proof                                        (*<->*)

| Command of user_cmd                                          (*-->*)

| Request of string | Message of string                        (*<--*) 

| Error_ of string  | System of string                         (*<--*)

| FoPpcFK of foppFK                                            (*-->*)

| FormKF of cellID * edit * indent * nest * cterm'             (*<--*)

| PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) (*<--*)

| RuleFK of tac                                              (*-->*)

| RuleKF of edit * tac                                       (*<--*)

| RefinedKF of (pblID * ((itm list) * ((bool * term) list))) (*<--*)

| Select of tac list                                         (*<--*)

| RefineKF of match list                                       (*<--*)

| Speed of int                                                 (*<--*)

| Active of int                                                (*<--*)

| Domain of domID;                                             (*<--*)

fun inout2str End_Proof = "End_Proof"

  | inout2str (Command user_cmd) = "Command "^(user_cmd2str user_cmd)

  | inout2str (Request s) = "Request "^s

  | inout2str (Message s) = "Message "^s

  | inout2str (Error_  s) = "Error_ "^s

  | inout2str (System  s) = "System "^s

  | inout2str (FoPpcFK foppFK) = "FoPpcFK "^(foppFK2str foppFK)

  | inout2str (FormKF (cellID, edit, indent, nest, ct')) =  

	       "FormKF ("^(string_of_int cellID)^","

	       ^(edit2str edit)^","^(string_of_int indent)^","

	       ^(nest2str nest)^",("

	       ^ct' ^")"

  | inout2str (PpcKF (cellID, edit, indent, nest, (pm,itemppc))) =

	       "PpcKF ("^(string_of_int cellID)^","

	       ^(edit2str edit)^","^(string_of_int indent)^","

	       ^(nest2str nest)^",("

	       ^(pblmet2str pm)^","^(itemppc2str itemppc)^"))"

  | inout2str (RuleKF (edit,tac)) = "RuleKF "^

	       pair2str(edit2str edit,tac2str tac)

  | inout2str (RuleFK tac) = "RuleFK "^(tac2str tac)  

  | inout2str (Select tacs)= 

	       "Select "^((strs2str' o (map tac2str)) tacs)

  | inout2str (RefineKF ms)  = "RefineKF "^(matchs2str ms)

  | inout2str (Speed i) = "Speed "^(string_of_int i)

  | inout2str (Active i) = "Active "^(string_of_int i)

  | inout2str (Domain dI) = "Domain "^dI;

fun inouts2str ios = (strs2str' o (map inout2str)) ios; 

datatype mout =

  Form' of inout         (* packing cterm' | cterm' ppc *)

| Problems of inout      (* passes specify (and solve)  *)

| Error' of inout

| EmptyMout;

fun mout2str (Form' inout) ="Form' "^(inout2str inout)

  | mout2str (Error'  inout) ="Error' "^(inout2str inout)

  | mout2str (EmptyMout    ) ="EmptyMout";

(*fun Form'2str (Form' )*)

(* init pbl with ...,dsc,empty | [] *)

fun init_pbl pbt = 

  let 

    fun pbt2itm (f,(d,t)) = 

      ((0,[],false,f,Inc((d,[]),(e_term,[]))):itm);

  in map pbt2itm pbt end;

(*take formal parameters from pbt, for transfer from pbl/met-hierarchy*)

fun init_pbl' pbt = 

  let 

    fun pbt2itm (f,(d,t)) = 

      ((0,[],false,f,Inc((d,[t]),(e_term,[]))):itm);

  in map pbt2itm pbt end;

(*generate 1 ppobj in ptree*)

fun generate1 thy (Add_Given' (_, itmlist)) Uistate (pos as (p,p_)) pt = 

    (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef,

			       (Upblmet,itms2itemppc thy [][]))),

     case p_ of Pbl => update_pbl pt p itmlist

	      | Met => update_met pt p itmlist)

  | generate1 thy (Add_Find' (_, itmlist)) Uistate (pos as (p,p_)) pt = 

    (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),

     case p_ of Pbl => update_pbl pt p itmlist

	      | Met => update_met pt p itmlist)

  | generate1 thy (Add_Relation' (_, itmlist)) Uistate (pos as (p,p_)) pt = 

    (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),

     case p_ of Pbl => update_pbl pt p itmlist

	      | Met => update_met pt p itmlist)

  | generate1 thy (Specify_Theory' domID) Uistate (pos as (p,_)) pt = 

    (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),

     update_domID pt p domID)

  | generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate 

	      (pos as (p,_)) pt = 

    let val pt = update_pbl pt p itms

	val pt = update_pblID pt p pI

    in ((p,Pbl),[],

	Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), 

	pt) end

  | generate1 thy (Specify_Method' (mID, oris, itms)) Uistate 

	      (pos as (p,_)) pt = 

    let val pt = update_oris pt p oris

	val pt = update_met pt p itms

	val pt = update_metID pt p mID

    in ((p,Met),[],

	Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), 

	pt) end

  | generate1 thy (Model_Problem' (_, itms)) Uistate (pos as (p,_)) pt =

(* val (itms,pos as (p,_)) = (pbl, pos);

   *)

    let val pt = update_pbl pt p itms

    in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef,

			   (Upblmet,itms2itemppc thy [][]))), pt) end

  | generate1 thy (Refine_Tacitly' (pI,pIre,domID,metID,pbl)) 

	      Uistate (pos as (p,_)) pt = 

    let val pt = update_pbl pt p pbl

	val pt = update_orispec pt p (domID,pIre,metID)

    in (pos,[],

	Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),

	pt) end

  | generate1 thy (Refine_Problem' (pI,_)) Uistate (pos as (p,_)) pt =

    let val (dI,_,mI) = get_obj g_spec pt p

	val pt = update_spec pt p (dI, pI, mI)

    in (pos,[],

	Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),pt)

    end

  | generate1 thy (Apply_Method' (_,topt, is)) _ (pos as (p,p_)) pt = 

    (writeln("###generate1 Apply_Method': pos = "^pos'2str (p,p_));

     writeln("###generate1 Apply_Method': topt= "^termopt2str topt);

     writeln("###generate1 Apply_Method': is  = "^istate2str is);

     case topt of 

	 Some t => 

	 let val (pt,_) = cappend_form pt p is t

	     val _= writeln("###generate1 Apply_Method: after cappend")

	 in (pos,[(*WN0502: pblnd generated without children*)], EmptyMout,pt)

	 end

       | None => 

	 (pos,[],EmptyMout,update_env pt p (Some is)))

  | generate1 thy (Take' t) l (p,p_) pt = (* val (Take' t) = m; *)

  let val p = let val (ps,p') = split_last p(*no connex to prev.ppobj*)

	    in if p'=0 then ps@[1] else p end;

    val (pt,c) = cappend_form pt p l t;

  in ((p,Frm):pos', c, 

      Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end

(* val (l, (p,p_)) = (RrlsState is, p);

   *)

  | generate1 thy (Begin_Trans' t) l (p,Frm) pt =

  let val (pt,c) = cappend_form pt p l t

      val pt = update_branch pt p TransitiveB (*040312*)

      (*replace the old PrfOjb ~~~~~*)

      val p = (lev_on o lev_dn(*starts with [...,0]*)) p; 

      val (pt,c) = cappend_form pt p l t;(*FIXME.0402 same istate ???*)

  in ((p,Frm), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), 

      pt) end

  | generate1 thy (Begin_Trans' t) l (p       ,Res) pt =

    (*append after existing PrfObj    _________*)

    generate1 thy (Begin_Trans' t) l (lev_on p,Frm) pt

  | generate1 thy (End_Trans' tasm) l (p,p_) pt =

  let val p' = lev_up p

      val (pt,c) = append_result pt p' l tasm Complete;

  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 =

  let val _= writeln("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));

      val (pt,c) = cappend_atomic pt p l 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 =

  let val _= writeln("###generate1 Rewrite': pos= "^pos'2str (p,p_))

      val (pt,c) = cappend_atomic pt p l 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')),

      pt)end

  | 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 =

(* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) = 

       (assoc_thy "Isac.thy", tac_, is, pos, pt);

   *)

  let val _= writeln("###generate1 Rewrite_Set_Inst': pos= "^pos'2str (p,p_))

      val (pt,c) = cappend_atomic pt p l 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 

      val pt = update_branch pt p TransitiveB (*040312*)

      val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) 

      val tac_ = Apply_Method' (e_metID, Some t, is)

      val pos' = ((lev_on o lev_dn) p, Frm)

  in (*implicit Take*) generate1 thy tac_ is pos' pt end

  | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt =

  let val _= writeln("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))

      val (pt,c) = cappend_atomic pt p l 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 

      val pt = update_branch pt p TransitiveB (*040312*)

      val is = init_istate (Rewrite_Set (id_rls rls)) 

      val tac_ = Apply_Method' (e_metID, Some t, is)

      val pos' = ((lev_on o lev_dn) p, Frm)

  in (*implicit Take*) generate1 thy tac_ is pos' pt end

  | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =

    let val _= writeln("###generate1 Check_Postcond': pos= "^pos'2str (p,p_))

       (*val (l',_) = get_obj g_loc pt p..don't overwrite with l from subpbl*)

	val (pt,c) = append_result pt p l (scval,map str2term asm) Complete

    in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), 

				   Nundef, term2str scval)), pt) end

  | generate1 thy (Calculate' (thy',op_,f,(f',thm'))) l (p,p_) pt =

  let val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f',[]) Complete;

  in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),

      pt)end

  | generate1 thy (Check_elementwise' (consts,pred,(f',asm))) l (p,p_) pt =

    let val _=writeln("###generate1 Check_elementwise': pos= "^pos'2str (p,p_))

	val (pt,c) = cappend_atomic pt p l consts 

	(Check_elementwise pred) (f',asm) Complete;

  in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),

      pt)end

  | generate1 thy (Or_to_List' (ors,list)) l (p,p_) pt =

    let val (pt,c) = cappend_atomic pt p l ors 

	Or_to_List (list,[]) Complete;

  in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str list)),

      pt)end

  | generate1 thy (Tac_ (_,f,id,f')) l (p,p_) pt =

    let val (pt,c) = cappend_atomic pt p l (str2term f) 

				    (Tac id) (str2term f',[]) Complete;

  in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f')), pt)end

  | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, f)) 

	      l (p,p_) pt =

    let val _=writeln("###generate1 Subproblem': pos= "^pos'2str (p,p_))

	val (pt,c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))

				     (oris, (domID, pblID, metID), hdl);

	(*val pbl = init_pbl ((#ppc o get_pbt) pblID);

	val pt = update_pblppc pt p pbl;--------4.9.03->Model_Problem*)

	(*val _= writeln("### generate1: is([3],Frm)= "^

		       (istate2str (get_istate pt ([3],Frm))));*)

	val f = Sign.string_of_term (sign_of thy) f;

    in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end

  | generate1 thy m' _ _ _ = 

    raise error ("generate1: not impl.for "^(tac_2str m'))

;

fun generate_hard thy m' (p,p_) pt =

  let  

    val p = case p_ of Frm => p | Res => lev_on p

  | _ => raise error ("generate_hard: call by "^(pos'2str (p,p_)));

  in generate1 thy m' e_istate (p,p_) pt end;

(*tacis are in reverse order from nxt_solve_/specify_: last = hd*)

fun generate ([]: taci list) ptp = 

    (writeln("### generate END-------------------------------");

     ptp)

(* val (tacis, (pt, _)) = (tacis, ptp);

   *)

  | generate tacis (pt, c, _:pos'(*!!dropped!!*)) = 

    let val (tacis', (_, tac_, (p, is))) = split_last tacis

	val (p',c',_,pt') = generate1 (assoc_thy "Isac.thy") tac_ is p pt

    in generate tacis' (pt', c@c', p') end;

(*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls       *

 *  of for connecting a user-input formula with the current calc-state.	     *

 *# It is somewhat incompatible with the rest of the math-engine:	     *

 *  (1) it is not created by a script					     *

 *  (2) thus there cannot be another user-input within a derivation	     *

 *# It suffers particularily from the not-well-foundedness of the math-engine*

 *  (1) FIXME other branchtyptes than Transitive will change 'embed_deriv'   *

 *  (2) FIXME and eventually 'compare_step' (ie. the script interpreter)     *

 *  (3) FIXME and eventually 'lev_back'                                      *

 *# Some improvements are evident FIXME.040215 '_deriv'ation:	             *

 *  (1) FIXME nest Rls_ in 'make_deriv'					     *

 *  (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus    *

 *	user-input will become possible in this part of a derivation	     *

 *  (3) FIXME do (2) only if a derivation has been found -- for efficiency,  *

 *	while a non-derivable inform requires to step until End_Proof'	     *

 *  (4) FIXME find criteria on when _not_ to step until End_Proof'           *

 *  (5) FIXME 

.*)

(*.update pos in tacis for embedding by generate.*)

(* val 

   *)

fun insert_pos _ [] = []

  | insert_pos (p:pos) (((tac,tac_,(_, ist))::tacis):taci list) = 

    ((tac,tac_,((p, Res), ist)):taci)

    ::((insert_pos (lev_on p) tacis):taci list);

(*.embed the tacis created by a '_deriv'ation;

  tacis are in order, thus are reverted for generate.*)

(* val (tacis, (pt, pos as (p, Frm))) =  (tacis', ptp);

   *)

fun embed_deriv (*[] ptp = ptp ...sys.form = input.form... excluded in inform

  | embed_deriv *)tacis (pt, pos as (p, Frm)) =

  (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402

    and transfer the istate (from _after_ compare_deriv) from Frm to Res*)

    let val (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = last_elem tacis

	val (Some ist,_) = get_obj g_loc pt p

	val form = get_obj g_form pt p

      (*val p = lev_on p; ---------------only difference*)

	val tacis = (Begin_Trans, Begin_Trans' form, (pos, Uistate))

		    ::(insert_pos ((lev_on o lev_dn) p) tacis)

		    @ [(End_Trans, End_Trans' (res, asm),

			(pos_plus (length tacis) (lev_dn p, Res), 

			 new_val res ist))]

	val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))

	val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))

	val pt = update_tac pt p (Derive (id_rls nrls))

        (*FIXME.040216 struct.ctree*)

	val pt = update_branch pt p TransitiveB

    in (c, (pt, pos)) end

(* val (tacis, (pt, pos as (p, Res))) =  (tacis', ptp);

   *)

  | embed_deriv tacis (pt, (p, Res)) =

  (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?

    and transfer the istate (from _after_ compare_deriv) from Res to new Res*)

    let val (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = last_elem tacis;

	val (_, Some ist) = get_obj g_loc pt p

	val (f,a) = get_obj g_result pt p

	val p = lev_on p;(*---------------only difference*)

	val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), Uistate))

		    ::(insert_pos ((lev_on o lev_dn) p) tacis)

		    @ [(End_Trans, End_Trans' (res, asm), 

			(pos_plus (length tacis) (lev_dn p, Res), 

			 new_val res ist))];

	val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))

	val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))

	val pt = update_tac pt p (Derive (id_rls nrls))

        (*FIXME.040216 struct.ctree*)

	val pt = update_branch pt p TransitiveB

    in (c, (pt, pos)) end;

(*

	val (_, Some ist) = get_obj g_loc pt p

	val (f,a) = get_obj g_result pt p

*)