1.1 --- a/src/sml/ME/script.sml	Fri Nov 03 14:30:32 2006 +0100
     1.2 +++ b/src/sml/ME/script.sml	Fri Nov 03 18:15:55 2006 +0100
     1.3 @@ -1869,12 +1869,12 @@
     1.4  
     1.5  (* val(thy, ptp as (pt,(p,_)), sc as Script (h $ body),ScrState (E,l,a,v,s,b))=
     1.6        ((thy',srls), (pt,pos),  sc,                     is);
     1.7 - *)
     1.8 +   *)
     1.9    | next_tac thy (ptp as (pt,(p,_)):ptree * pos') (sc as Script (h $ body)) 
    1.10  	     (ScrState (E,l,a,v,s,b)) =
    1.11    ((*writeln("### next_tac-----------------: E= ");
    1.12     writeln( istate2str (ScrState (E,l,a,v,s,b)));*)
    1.13 -   case if l=[] then appy thy ptp E [R] body None e_term
    1.14 +   case if l=[] then appy thy ptp E [R] body None v
    1.15         else nstep_up thy ptp sc E l Skip_ a v of
    1.16        Skip (v,_) =>                                              (*finished*)
    1.17        (case par_pbl_det pt p of

     2.1 --- a/src/smltest/IsacKnowledge/simplify.sml	Fri Nov 03 14:30:32 2006 +0100
     2.2 +++ b/src/smltest/IsacKnowledge/simplify.sml	Fri Nov 03 18:15:55 2006 +0100
     2.3 @@ -12,6 +12,7 @@
     2.4  "table of contents -----------------------------------------------";
     2.5  "-----------------------------------------------------------------";
     2.6  "----------- CAS-command Simplify --------------------------------";
     2.7 +"----------- append inform with final result ---------------------";
     2.8  "-----------------------------------------------------------------";
     2.9  "-----------------------------------------------------------------";
    2.10  "-----------------------------------------------------------------";
    2.11 @@ -34,20 +35,22 @@
    2.12  else raise error "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)";
    2.13  
    2.14  
    2.15 +"----------- append inform with final result ---------------------";
    2.16 +"----------- append inform with final result ---------------------";
    2.17 +"----------- append inform with final result ---------------------";
    2.18 +states:=[];
    2.19 +CalcTree [(["term ((14 * x * y) / ( x * y ))", "normalform N"],
    2.20 +	   ("Rational.thy",["rational","simplification"],
    2.21 +	    ["simplification","of_rationals"]))];
    2.22 +Iterator 1;
    2.23 +moveActiveRoot 1;
    2.24 +autoCalculate 1 CompleteCalcHead;
    2.25 +autoCalculate 1 (Step 1);
    2.26 +appendFormula 1 "14";
    2.27 +val ((pt,p),_) = get_calc 1; show_pt pt;
    2.28  
    2.29 -
    2.30 -
    2.31 -
    2.32 -
    2.33 -
    2.34 -
    2.35 -
    2.36 -
    2.37 -
    2.38 -
    2.39 -
    2.40 -
    2.41 -
    2.42 -
    2.43 -
    2.44 -
    2.45 +autoCalculate 1 (Step 1);
    2.46 +val ((pt,p),_) = get_calc 1; show_pt pt;
    2.47 +val Form res = (#1 o pt_extract) (pt, ([],Res));
    2.48 +if p = ([], Res) andalso term2str res = "14" then ()
    2.49 +else raise error "simplify.sml: append inform with final result ?!?";