1.1 --- a/src/Tools/isac/Scripts/scrtools.sml	Thu Aug 12 15:08:12 2010 +0200
     1.2 +++ b/src/Tools/isac/Scripts/scrtools.sml	Mon Aug 16 16:19:53 2010 +0200
     1.3 @@ -349,19 +349,18 @@
     1.4  	\   (Try (Repeat (Rewrite_Inst [(bdv,v)] real_add_commute False))) @@\
     1.5  	\   (Try (Repeat (Rewrite_Inst [(bdv,v)] real_mult_commute False)))) \
     1.6  	\  t)"; 
     1.7 -val Repeat $ _ = 
     1.8 +val Repeat $ _ =
     1.9      ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) 
    1.10  	"Repeat (Rewrite real_diff_minus False t)";
    1.11  val Try $ _ = 
    1.12      ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) 
    1.13  	"Try (Rewrite real_diff_minus False t)";
    1.14 -(*
    1.15  val Cal $ _ =
    1.16      ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) 
    1.17 -	"Calculate plus";
    1.18 +	"Calculate PLUS";
    1.19  val Ca1 $ _ =
    1.20      ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) 
    1.21 -	"Calculate1 plus";
    1.22 +	"Calculate1 PLUS";
    1.23  val Rew $ (Free (_,IDtype)) $ _ $ t =
    1.24      ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) 
    1.25  	"Rewrite real_diff_minus False t";
    1.26 @@ -444,20 +443,20 @@
    1.27      raise error ("contain_bdv called with ["^(id_rule r)^",...]");
    1.28  
    1.29  
    1.30 -fun rules2scr_Rls calc rules = 
    1.31 +fun rules2scr_Rls calc rules = (*WN100816 t_ -> e_term without understanding*)
    1.32      if contain_bdv rules
    1.33      then ScrStep_inst $ Term $ Bdv $ 
    1.34 -	 (Repeat $ (((@@ o (map (rule2stac_inst calc))) rules) $ t_))
    1.35 +	 (Repeat $ (((@@ o (map (rule2stac_inst calc))) rules) $ e_term))
    1.36      else ScrStep $ Term $
    1.37 -	 (Repeat $ (((@@ o (map (rule2stac      calc))) rules) $ t_));
    1.38 +	 (Repeat $ (((@@ o (map (rule2stac      calc))) rules) $ e_term));
    1.39  (* val (calc, rules) = (!calclist', rules);
    1.40     *)
    1.41 -fun rules2scr_Seq calc rules =
    1.42 +fun rules2scr_Seq calc rules = (*WN100816 t_ -> e_term without understanding*)
    1.43      if contain_bdv rules
    1.44      then ScrStep_inst $ Term $ Bdv $ 
    1.45 -	 (((@@ o (map (rule2stac_inst calc))) rules) $ t_)
    1.46 +	 (((@@ o (map (rule2stac_inst calc))) rules) $ e_term)
    1.47      else ScrStep $ Term $
    1.48 -	 (((@@ o (map (rule2stac      calc))) rules) $ t_);
    1.49 +	 (((@@ o (map (rule2stac      calc))) rules) $ e_term);
    1.50  
    1.51  (*.prepare the input for an rls for use:
    1.52     # generate a script for stepwise execution of the rls
    1.53 @@ -491,5 +490,3 @@
    1.54   val Script sc = (#scr o rep_rls o prep_rls) isolate_bdv;
    1.55   (writeln o term2str) sc;
    1.56    *)
    1.57 -
    1.58 -----bootstrapping---*)