1.1 --- a/src/Tools/isac/Interpret/script.sml	Thu Sep 22 14:43:47 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri Sep 23 08:30:35 2011 +0200
     1.3 @@ -976,8 +976,9 @@
     1.4    | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2) =
     1.5        (case assy ya ((E,(l@[L,R]),a,v,S,b),ss) e1 of
     1.6  	       NasNap (v, E) => assy ya ((E,(l@[R]),a,v,S,b),ss) e2
     1.7 -       | ay => (ay)) 
     1.8 +       | ay => (ay))
     1.9  
    1.10 +    (*here is not a tactical like TRY etc, but a tactic creating a step in calculation*)
    1.11    | assy (((thy',sr),d),ap) (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
    1.12        (case handle_leaf "locate" thy' sr E a v t of
    1.13  	       (a', Expr s) => 
    1.14 @@ -1494,8 +1495,6 @@
    1.15     20.8.02: do NOT return safe (is only changed in locate !!!)
    1.16  *)
    1.17  fun next_tac (thy,_) (pt,p) (Rfuns {next_rule,...}) (RrlsState(f,f',rss,_), ctxt) =
    1.18 -      let val ctxt = get_ctxt pt p
    1.19 -      in
    1.20          if f = f'
    1.21          then (End_Detail' (f',[])(*8.6.03*), (Uistate, ctxt), 
    1.22    		    (f', Sundef(*FIXME is no value of next_tac! vor 8.6.03*)))  (*finished*)
    1.23 @@ -1506,12 +1505,9 @@
    1.24    	          (Rewrite' (thy, "e_rew_ord", e_rls,(*!?!8.6.03*) false,
    1.25    			       (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])),
    1.26    	           (Uistate, ctxt), (e_term, Sundef)))                    (*next stac*)
    1.27 -      end
    1.28  
    1.29    | next_tac thy (ptp as (pt, pos as (p, _)):ptree * pos') (sc as Script (h $ body)) 
    1.30  	  (ScrState (E,l,a,v,s,b), ctxt) =
    1.31 -      let val ctxt = get_ctxt pt pos (*WN110518 we have ctxt twice -- redesign*)
    1.32 -      in
    1.33          (case if l = [] 
    1.34                then appy thy ptp E [R] body NONE v
    1.35                else nstep_up thy ptp sc E l Skip_ a v of
    1.36 @@ -1527,7 +1523,6 @@
    1.37           | Napp _ => (Empty_Tac_, (e_istate, ctxt), (e_term, Sundef)) (*helpless*)
    1.38           | Appy (m', scrst as (_,_,_,v,_,_)) => 
    1.39               (m', (ScrState scrst, ctxt), (v, Sundef)))               (*next stac*)
    1.40 -      end
    1.41  
    1.42    | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (istate2str is));
    1.43