1.1 --- a/src/Tools/isac/Interpret/script.sml	Tue May 17 15:02:43 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Tue May 17 17:38:35 2011 +0200
     1.3 @@ -183,8 +183,7 @@
     1.4        | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_,_,e2)) a = 
     1.5      	(case get_t y e1 a of NONE => get_t y e2 a | la => la)
     1.6      (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
     1.7 -    	(tracing("get_t: Let e1= "^(term2str e1)^", e2= "^(term2str e2));
     1.8 -	 case get_t y e1 a of NONE => get_t y e2 a | la => la)
     1.9 +	    (case get_t y e1 a of NONE => get_t y e2 a | la => la)
    1.10        | get_t y (Abs (_,_,e)) a = get_t y e a*)
    1.11        | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
    1.12      	get_t y e1 a (*don't go deeper without evaluation !*)
    1.13 @@ -1653,6 +1652,7 @@
    1.14    			       (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])),
    1.15    	           (Uistate, ctxt), (e_term, Sundef)))                    (*next stac*)
    1.16        end
    1.17 +
    1.18    | next_tac thy (ptp as (pt,pos as (p,_)):ptree * pos') (sc as Script (h $ body)) 
    1.19  	  (ScrState (E,l,a,v,s,b), ctxt) =
    1.20        let val ctxt = get_ctxt pt pos
    1.21 @@ -1673,11 +1673,12 @@
    1.22           | Appy (m', scrst as (_,_,_,v,_,_)) => 
    1.23               (m', (ScrState scrst, ctxt), (v, Sundef)))               (*next stac*)
    1.24        end
    1.25 +
    1.26    | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (istate2str is));
    1.27  
    1.28  
    1.29  (*.create the initial interpreter state from the items of the guard.*)
    1.30 -fun init_scrstate thy itms metID =
    1.31 +fun init_scrstate thy itms metID =(*FIXME.WN170511: delete ctxt from value*)
    1.32    let
    1.33      val actuals = itms2args thy metID itms;
    1.34  	  val scr as Script sc = (#scr o get_met) metID;