val next_tac : (*diss: next-tactic-function*)

     Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> Selem.istate * 'a -> Tac.tac_ * (Selem.istate * 'a) * (term * Selem.safe)

   val stac2tac_ : Ctree.ctree -> theory -> term -> Tac.tac * Tac.tac_

   val tac_2res : Tac.tac_ -> term

   val upd_env_opt : LTool.env -> term option * term -> LTool.env

 fun appy thy ptp E l (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =

     (case appy thy ptp E (l @ [Celem.L, Celem.R]) e a v of

       Skip (res, E) => 

         let val E' = LTool.upd_env E (Free (i,T), res);

         in appy thy ptp E' (l @ [Celem.R, Celem.D]) b a v end

     | ay => ay)

   | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*1*),_) $ c $ e $ a) _ v =

     (if Rewrite.eval_true_ th sr (subst_atomic (LTool.upd_env E (a,v)) c)

      then appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v

      else Skip (v, E))

   | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*2*),_) $ c $ e) a v =

     (if Rewrite.eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)

      then appy thy ptp E (l @ [Celem.R]) e a v

      else Skip (v, E))

   | appy (thy as (th,sr)) ptp E l (Const ("If",_) $ c $ e1 $ e2) a v =

     (if Rewrite.eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)

      then appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v

      else appy thy ptp E (l @ [Celem.R]) e2 a v)

   | appy thy ptp E l (Const ("Script.Repeat"(*1*),_) $ e $ a) _ v = 

     appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v

   | appy thy ptp E l (Const ("Script.Repeat"(*2*),_) $ e) a v = appy thy ptp E (l @ [Celem.R]) e a v

   | appy thy ptp E l (Const ("Script.Try"(*2*),_) $ e $ a) _ v =

     (case appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v of

       Napp E => (Skip (v, E))

     | ay => ay)

   | appy thy ptp E l(Const ("Script.Try"(*1*),_) $ e) a v =

     (case appy thy ptp E (l @ [Celem.R]) e a v of

       Napp E => (Skip (v, E))

     | ay => ay)

   | appy thy ptp E l (Const ("Script.Or"(*1*),_) $e1 $ e2 $ a) _ v =

     (case appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v of

 	    Appy lme => Appy lme

     | _ => appy thy ptp E (*LTool.env*) (l @ [Celem.L, Celem.R]) e2 (SOME a) v)

   | appy thy ptp E l (Const ("Script.Or"(*2*),_) $e1 $ e2) a v =

     (case appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v of

 	    Appy lme => Appy lme

     | _ => appy thy ptp E (l @ [Celem.R]) e2 a v)

   | appy thy ptp E l (Const ("Script.Seq"(*2*),_) $ e1 $ e2 $ a) _ v =

     (case appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v of

 	    Skip (v,E) => appy thy ptp E (l @ [Celem.L, Celem.R]) e2 (SOME a) v

     | ay => ay)

   | appy thy ptp E l (Const ("Script.Seq"(*1*),_) $ e1 $ e2) a v =

     (case appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v of

 	    Skip (v,E) => appy thy ptp E (l @ [Celem.R]) e2 a v

     | ay => ay)

   (* a leaf has been found *)   

   | appy ((th,sr)) (pt, p) E l t a v =

     case handle_leaf "next  " th sr E a v t of

 	    (_, LTool.Expr s) => Skip (s, E)

     | (a', LTool.STac stac) =>

 	    let val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac

       in case m of

 	      Tac.Subproblem _ => Appy (m', (E,l,a',tac_2res m',Selem.Sundef,false))

 	    | _ =>

         (case Applicable.applicable_in p pt m of

 		       Chead.Appl m' => (Appy (m', (E,l,a',tac_2res m',Selem.Sundef,false)))

 		     | _ => Napp E)

 	    end

 fun nxt_up thy ptp (scr as (Rule.Prog sc)) E l ay (Const ("HOL.Let", _) $ _) a v = (*comes from let=...*)

     if ay = Napp_

     then nstep_up thy ptp scr E (drop_last l) Napp_ a v

     else (*Skip_*)

 	    let

         val up = drop_last l

         val (i, T, body) =

           (case go up sc of

              Const ("HOL.Let",_) $ _ $ (Abs aa) => aa

            | t => error ("nxt_up..HOL.Let $ _ with " ^ Rule.term2str t))

         val i = TermC.mk_Free (i, T)

         val E = LTool.upd_env E (i, v)

       in

         case appy thy ptp E (up @ [Celem.R, Celem.D]) body a v  of

 	        Appy lre => Appy lre

 	      | Napp E => nstep_up thy ptp scr E up Napp_ a v

 	      | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v

 	    end

   | nxt_up thy ptp scr E l ay (Abs _) a v =  nstep_up thy ptp scr E l ay a v

   | nxt_up thy ptp scr E l ay (Const ("HOL.Let",_) $ _ $ (Abs _)) a v =

     nstep_up thy ptp scr E l ay a v

   (*no appy_: never causes Napp -> Helpless*)

   | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*1*), _) $ c $ e $ _) a v = 

     if Rewrite.eval_true_ th sr (subst_atomic (upd_env_opt E (a, v)) c) 

     then case appy thy ptp E (l @ [Celem.L, Celem.R]) e a v of

 	     Appy lr => Appy lr

 	  | Napp E => nstep_up thy ptp scr E l Skip_ a v

 	  | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v

     else nstep_up thy ptp scr E l Skip_ a v

   (*no appy_: never causes Napp - Helpless*)

   | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*2*), _) $ c $ e) a v = 

     if Rewrite.eval_true_ th sr (subst_atomic (upd_env_opt E (a, v)) c) 

     then case appy thy ptp E (l @ [Celem.R]) e a v of

 	    Appy lr => Appy lr

 	  | Napp E => nstep_up thy ptp scr E l Skip_ a v

 	  | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v

     else nstep_up thy ptp scr E l Skip_ a v

   | nxt_up thy ptp scr E l ay (Const ("If", _) $ _ $ _ $ _) a v = nstep_up thy ptp scr E l ay a v

   | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)

       (Const ("Script.Repeat"(*1*), _) $ e $ _) a v =

     (case appy thy ptp (*upd_env*) E (*a,v)*) (l @ [Celem.L, Celem.R]) e a v  of

       Appy lr => Appy lr

     | Napp E =>  nstep_up thy ptp scr E l Skip_ a v

     | Skip (v,E) =>  nstep_up thy ptp scr E l Skip_ a v)

   | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)

       (Const ("Script.Repeat"(*2*), _) $ e) a v =

     (case appy thy ptp (*upd_env*) E (*a,v)*) (l @ [Celem.R]) e a v  of

       Appy lr => Appy lr

     | Napp E => nstep_up thy ptp scr E l Skip_ a v

     | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v)

   | nxt_up thy ptp scr E l _ (Const ("Script.Try"(*2*),_) $ _ $ _) a v = (*makes Napp to Skip*)

     nstep_up thy ptp scr E l Skip_ a v

   | nxt_up thy ptp scr E l _ (Const ("Script.Try"(*1*), _) $ _) a v = (*makes Napp to Skip*)

     nstep_up thy ptp scr E l Skip_ a v

   | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ $ _ $ _) a v =

     nstep_up thy ptp scr E l ay a v

   | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ $ _) a v = nstep_up thy ptp scr E l ay a v

   | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ ) a v = 

     nstep_up thy ptp scr E (drop_last l) ay a v

   | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*1*),_) $ _ $ _ $ _) a v =

     (*all has been done in (*2*) below*) nstep_up thy ptp scr E l ay a v

   | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*2*),_) $ _ $ _) a v = (*comes from e2*)

     nstep_up thy ptp scr E l ay a v

   | nxt_up thy ptp (scr as Rule.Prog sc) E l ay (Const ("Script.Seq"(*3*),_) $ _) a v = (*comes from e1*)

     if ay = Napp_

     then nstep_up thy ptp scr E (drop_last l) Napp_ a v

     else (*Skip_*)

       let val up = drop_last l;

           val e2 =

             (case go up sc of

                Const ("Script.Seq"(*2*), _) $ _ $ e2 => e2

              | t => error ("nxt_up..Script.Seq $ _ with " ^ Rule.term2str t))

       in case appy thy ptp E (up @ [Celem.R]) e2 a v  of

         Appy lr => Appy lr

       | Napp E => nstep_up thy ptp scr E up Napp_ a v

       | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end

   | nxt_up _ _ _ _ _ _ t _ _ = error ("nxt_up not impl for " ^ Rule.term2str t)

 and nstep_up thy ptp (Rule.Prog sc) E l ay a v = 

     if 1 < length l

     then 

       let val up = drop_last l; 

       in (nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v ) end

     else (*interpreted to end*)

       if ay = Skip_ then Skip (v, E) else Napp E 

   | nstep_up _ _ _ _ l _ _ _ = error ("nstep_up: uncovered fun-def at " ^ Celem.loc_2str l)

 (* decide for the next applicable stac in the script;

    returns (stactic, value) - the value in case the script is finished 

    12.8.02:         ~~~~~ and no assumptions ??? FIXME ???

    20.8.02: must return p in case of finished, because the next script

             consulted need not be the calling script:

             in case of detail ie. _inserted_ PrfObjs, the next stac

             has to searched in a script with PblObj.status<>Complete !

             (.. not true for other details ..PrfObj ??????????????????

    20.8.02: do NOT return safe (is only changed in locate !!!)

 *)

 fun next_tac (thy,_) _ (Rule.Rfuns {next_rule, ...}) (Selem.RrlsState(f, f', rss, _), ctxt) =

     if f = f'

     then (Tac.End_Detail' (f',[])(*8.6.03*), (Selem.Uistate, ctxt), 

     	(f', Selem.Sundef(*FIXME is no value of next_tac! vor 8.6.03*)))                (*finished*)

     else

       (case next_rule rss f of

     	  NONE => (Tac.Empty_Tac_, (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef))       (*helpless*)

     	| SOME (Rule.Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) => 

     	    (Tac.Rewrite' (thy, "e_rew_ord", Rule.e_rls, false, thm'', f, (Rule.e_term, [(*!?!8.6.03*)])),

   	         (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef))                          (*next stac*)

       | _ => error "next_tac: uncovered case next_rule")

   | next_tac thy (ptp as (pt, (p, _))) (sc as Rule.Prog prog) 

 	    (Selem.ScrState (E,l,a,v,s,_), ctxt) =

     (case if l = [] then appy thy ptp E [Celem.R] (LTool.body_of prog) NONE v

           else nstep_up thy ptp sc E l Skip_ a v of

        Skip (v, _) =>                                                                 (*finished*)

          (case par_pbl_det pt p of

 	          (true, p', _) => 

 	             let

 	               val (_,pblID,_) = get_obj g_spec pt p';

 	              in (Tac.Check_Postcond' (pblID, (v, [(*assigned in next step*)])), 

 	                   (Selem.e_istate, ctxt), (v,s)) 

                 end

 	        | _ => (Tac.End_Detail' (Rule.e_term,[])(*8.6.03*), (Selem.e_istate, ctxt), (v,s)))

      | Napp _ => (Tac.Empty_Tac_, (Selem.e_istate, ctxt), (Rule.e_term, Selem.Sundef))     (*helpless*)

      | Appy (m', scrst as (_,_,_,v,_,_)) =>

          (m', (Selem.ScrState scrst, ctxt), (v, Selem.Sundef)))                      (*next stac*)

   | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (Selem.istate2str is));