1.1 --- a/src/Tools/isac/Interpret/ctree.sml	Sun May 15 13:59:05 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Tue May 17 09:55:30 2011 +0200
     1.3 @@ -256,23 +256,11 @@
     1.4  					    only used during ass_dn/up*)
     1.5  val e_scrstate = ([],[],NONE,e_term,Sundef,false):scrstate;
     1.6  
     1.7 -
     1.8 -(*21.8.02 ---> definitions.sml for datatype scr 
     1.9 -type rrlsstate =      (*state for reverse rewriting*)
    1.10 -     (term *          (*the current formula*)
    1.11 -      rule list      (*of reverse rewrite set (#1#)*)
    1.12 -	    list *    (*may be serveral, eg. in norm_rational*)
    1.13 -      (rule *         (*Thm (+ Thm generated from Calc) resulting in ...*)
    1.14 -       (term *        (*... rewrite with ...*)
    1.15 -	term list))   (*... assumptions*)
    1.16 -	  list);      (*derivation from given term to normalform
    1.17 -		       in reverse order with sym_thm; 
    1.18 -                       (#1#) could be extracted from here #1*) --------*)
    1.19 -     
    1.20 -datatype istate =     (*interpreter state*)
    1.21 -	 Uistate                 (*undefined in modspec, in '_deriv'ation*)
    1.22 -       | ScrState of scrstate    (*for script interpreter*)
    1.23 -       | RrlsState of rrlsstate; (*for reverse rewriting*)
    1.24 +(* for handling type istate see fun from_pblobj_or_detail', +? *)
    1.25 +datatype istate =           (*interpreter state*)
    1.26 +	  Uistate                 (*undefined in modspec, in '_deriv'ation*)
    1.27 +  | ScrState of scrstate    (*for script interpreter*)
    1.28 +  | RrlsState of rrlsstate; (*for reverse rewriting*)
    1.29  val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false)):istate;
    1.30  val e_ctxt = ProofContext.init_global @{theory "Pure"};
    1.31  
    1.32 @@ -1280,7 +1268,8 @@
    1.33                                         1.00 not used anymore*)
    1.34  
    1.35  (*FIXME.WN.12.03: update_X X pos pt -> pt could be chained by o (efficiency?)*)
    1.36 -fun update_ctxt   pt pos x = appl_obj (repl_ctxt   x) pt pos;
    1.37 +fun update_ctxt   pt pos x = appl_obj (repl_ctxt   x) pt pos; (*for use on PblObj, 
    1.38 +otherwise use generate1; compare fun get_ctxt*)
    1.39  fun update_env    pt pos x = appl_obj (repl_env    x) pt pos;
    1.40  fun update_domID  pt pos x = appl_obj (repl_domID  x) pt pos;
    1.41  fun update_pblID  pt pos x = appl_obj (repl_pblID  x) pt pos;