1.1 --- a/src/Tools/isac/Interpret/ctree.sml	Wed May 18 09:25:36 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Wed May 18 09:32:26 2011 +0200
     1.3 @@ -172,10 +172,10 @@
     1.4    | pos_2str Und = "Und";
     1.5  
     1.6  type pos' = pos * pos_;
     1.7 -(*WN.12.03 remembering interator (pos * pos_) for ptree 
     1.8 +(*WN0312 remembering interator (pos * pos_) for ptree 
     1.9  	   pos : lev_on, lev_dn, lev_up, 
    1.10 -                 lev_onFrm, lev_dnRes (..see solve Apply_Method !) 
    1.11 -           pos_:
    1.12 +           lev_onFrm, lev_dnRes (..see solve Apply_Method !) 
    1.13 +     pos_:
    1.14  # generate1 sets pos_ if possible  ...?WN0502?NOT...
    1.15  # generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn
    1.16                       exceptions: Begin/End_Trans
    1.17 @@ -1269,7 +1269,7 @@
    1.18  
    1.19  (*FIXME.WN.12.03: update_X X pos pt -> pt could be chained by o (efficiency?)*)
    1.20  fun update_ctxt   pt pos x = appl_obj (repl_ctxt   x) pt pos; (*for use on PblObj, 
    1.21 -otherwise use generate1; compare fun get_ctxt*)
    1.22 +otherwise use fun generate1; compare fun get_ctxt*)
    1.23  fun update_env    pt pos x = appl_obj (repl_env    x) pt pos;
    1.24  fun update_domID  pt pos x = appl_obj (repl_domID  x) pt pos;
    1.25  fun update_pblID  pt pos x = appl_obj (repl_pblID  x) pt pos;

     2.1 --- a/src/Tools/isac/Interpret/script.sml	Wed May 18 09:25:36 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/script.sml	Wed May 18 09:32:26 2011 +0200
     2.3 @@ -1217,9 +1217,6 @@
     2.4            NOT IMPL. -- "error: do other step before"
     2.5     NotLocatable: thus generate_hard
     2.6  *)
     2.7 -(* val (Rewrite'(_,ro,er,pa,(id,str),f,_), p, Rfuns {locate_rule=lo,...},
     2.8 -	RrlsState (_,f'',rss,rts)) = (m, (p,p_), sc, is);
     2.9 -   *)
    2.10  fun locate_gen (thy',_) (Rewrite'(_,ro,er,pa,(id,str),f,_)) (pt,p) 
    2.11  	       (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) = 
    2.12      (case lo rss f (Thm (id, mk_thm (assoc_thy thy') str)) of