1.1 --- a/src/Tools/isac/Interpret/script.sml	Wed Jul 20 13:05:48 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Wed Jul 20 14:55:29 2011 +0200
     1.3 @@ -1015,41 +1015,35 @@
     1.4  		             )
     1.5             end);
     1.6  
     1.7 -fun ass_up (ys as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss) 
     1.8 -	   (Const ("HOL.Let",_) $ _) =
     1.9 -    let (*val _= tracing("### ass_up1 Let$e: is=")
    1.10 -	val _= tracing(istate2str (ScrState is))*)
    1.11 -	val l = drop_last l; (*comes from e, goes to Abs*)
    1.12 -      val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
    1.13 -      val i = mk_Free (i, T);
    1.14 -      val E = upd_env E (i, v);
    1.15 -      (*val _=tracing("### ass_up2 Let$e: E="^(subst2str E));*)
    1.16 -    in case assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body of
    1.17 -	   Assoc iss => Assoc iss
    1.18 -	 | NasApp iss => astep_up ys iss 
    1.19 -	 | NasNap (v, E) => astep_up ys ((E,l,a,v,S,b),ss) end
    1.20 +fun ass_up (ys as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ _) =
    1.21 +      let 
    1.22 +        (*val _= tracing("### ass_up1 Let$e: is=")
    1.23 +	      val _= tracing(istate2str (ScrState is))*)
    1.24 +	      val l = drop_last l; (*comes from e, goes to Abs*)
    1.25 +        val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
    1.26 +        val i = mk_Free (i, T);
    1.27 +        val E = upd_env E (i, v);
    1.28 +        (*val _=tracing("### ass_up2 Let$e: E="^(subst2str E));*)
    1.29 +       in case assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body of
    1.30 +	          Assoc iss => Assoc iss
    1.31 +	        | NasApp iss => astep_up ys iss 
    1.32 +	        | NasNap (v, E) => astep_up ys ((E,l,a,v,S,b),ss) end
    1.33  
    1.34    | ass_up ys (iss as (is,_)) (Abs (_,_,_)) = 
    1.35 -    ((*tracing("### ass_up  Abs: is=");
    1.36 -     tracing(istate2str (ScrState is));*)
    1.37 -     astep_up ys iss) (*TODO 5.9.00: env ?*)
    1.38 +      ((*tracing("### ass_up  Abs: is=");
    1.39 +      tracing(istate2str (ScrState is));*)
    1.40 +      astep_up ys iss) (*TODO 5.9.00: env ?*)
    1.41  
    1.42    | ass_up ys (iss as (is,_)) (Const ("HOL.Let",_) $ e $ (Abs (i,T,b)))=
    1.43 -    ((*tracing("### ass_up Let $ e $ Abs: is=");
    1.44 -     tracing(istate2str (ScrState is));*)
    1.45 -     astep_up ys iss) (*TODO 5.9.00: env ?*)
    1.46 +      ((*tracing("### ass_up Let $ e $ Abs: is=");
    1.47 +      tracing(istate2str (ScrState is));*)
    1.48 +      astep_up ys iss) (*TODO 5.9.00: env ?*)
    1.49  
    1.50 -    (* val (ysa, iss,                 (Const ("Script.Seq",_) $ _ $ _ $ _)) =
    1.51 -	   (ys,  ((E,up,a,v,S,b),ss), (go up sc));
    1.52 -       *)
    1.53    | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _ $ _) =
    1.54 -    astep_up ysa iss (*all has been done in (*2*) below*)
    1.55 +      astep_up ysa iss (*all has been done in (*2*) below*)
    1.56  
    1.57    | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _) =
    1.58 -    (* val (ysa, iss,                 (Const ("Script.Seq",_) $ _ $ _)) =
    1.59 -	   (ys,  ((E,up,a,v,S,b),ss), (go up sc));
    1.60 -       *)
    1.61 -    astep_up ysa iss (*2*: comes from e2*)
    1.62 +      astep_up ysa iss (*2*: comes from e2*)
    1.63  
    1.64    | ass_up (ysa as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
    1.65  	   (Const ("Script.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*)