1.1 --- a/src/Tools/isac/calcelems.sml	Tue Sep 28 13:30:29 2010 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Fri Oct 01 10:23:38 2010 +0200
     1.3 @@ -117,17 +117,16 @@
     1.4      difference: there is always _ONE_ redex rewritten in 1 call,
     1.5      thus wrap Rrls by: Rls (Rls_ ...)*)
     1.6    
     1.7 -  | Rrls of (*for 'reverse rewriting' by SML-functions instead Script*)
     1.8 -    {id : string,          (*for trace_rewrite:=true                 *)
     1.9 -     prepat  : (term list *(*preconds, eval with subst from pattern  *)
    1.10 -		term )     (*pattern matched in subterms             *)
    1.11 -		   list,   (*meta-conjunction is or                  *)
    1.12 -     rew_ord  : rew_ord,   (*for rules                               *)
    1.13 -     erls     : rls,       (*for the conditions in rules and pat     *)
    1.14 -     (*            '^ because of rewrite in applicable_in
    1.15 -						compare type met*)
    1.16 -     calc     : calc list, (*for Calculate in scr, set by prep_rls *)
    1.17 -     scr      : scr}; (*Rfuns {...}  (how to restrict type ???)*)
    1.18 +  | Rrls of (* for 'reverse rewriting' by SML-functions instead Script        *)
    1.19 +    {id : string,          (* for trace_rewrite := true                       *)
    1.20 +     prepat  : (term list *(* preconds, eval with subst from pattern;  
    1.21 +                              if [HOLogic.true_const], match decides alone    *)
    1.22 +		term )     (* pattern matched with current (sub)term          *)
    1.23 +		   list,   (* meta-conjunction is or                          *)
    1.24 +     rew_ord  : rew_ord,   (* for rules                                       *)
    1.25 +     erls     : rls,       (* for the conditions in rules and preconds        *)
    1.26 +     calc     : calc list, (* for Calculate in scr, set automatic.in prep_rls *)
    1.27 +     scr      : scr};      (* Rfuns {...}  (how to restrict type ???)         *)
    1.28  (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently
    1.29    from rls, and then contain both Script _AND_ Rfuns !!!*)
    1.30