# HG changeset patch
# User wneuper
# Date 1162574155 -3600
# Node ID 634a6268de8105cdbfcb3827ff1ed923de750028
# Parent  6361fdad1d9468098dfe72dbca015b13dc423364
bugfix for inform with final result (gave ??.empty at ([],Res))

diff -r 6361fdad1d94 -r 634a6268de81 src/sml/ME/script.sml
--- a/src/sml/ME/script.sml	Fri Nov 03 14:30:32 2006 +0100
+++ b/src/sml/ME/script.sml	Fri Nov 03 18:15:55 2006 +0100
@@ -1869,12 +1869,12 @@
 
 (* val(thy, ptp as (pt,(p,_)), sc as Script (h $ body),ScrState (E,l,a,v,s,b))=
       ((thy',srls), (pt,pos),  sc,                     is);
- *)
+   *)
   | next_tac thy (ptp as (pt,(p,_)):ptree * pos') (sc as Script (h $ body)) 
 	     (ScrState (E,l,a,v,s,b)) =
   ((*writeln("### next_tac-----------------: E= ");
    writeln( istate2str (ScrState (E,l,a,v,s,b)));*)
-   case if l=[] then appy thy ptp E [R] body None e_term
+   case if l=[] then appy thy ptp E [R] body None v
        else nstep_up thy ptp sc E l Skip_ a v of
       Skip (v,_) =>                                              (*finished*)
       (case par_pbl_det pt p of
diff -r 6361fdad1d94 -r 634a6268de81 src/smltest/IsacKnowledge/simplify.sml
--- a/src/smltest/IsacKnowledge/simplify.sml	Fri Nov 03 14:30:32 2006 +0100
+++ b/src/smltest/IsacKnowledge/simplify.sml	Fri Nov 03 18:15:55 2006 +0100
@@ -12,6 +12,7 @@
 "table of contents -----------------------------------------------";
 "-----------------------------------------------------------------";
 "----------- CAS-command Simplify --------------------------------";
+"----------- append inform with final result ---------------------";
 "-----------------------------------------------------------------";
 "-----------------------------------------------------------------";
 "-----------------------------------------------------------------";
@@ -34,20 +35,22 @@
 else raise error "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)";
 
 
+"----------- append inform with final result ---------------------";
+"----------- append inform with final result ---------------------";
+"----------- append inform with final result ---------------------";
+states:=[];
+CalcTree [(["term ((14 * x * y) / ( x * y ))", "normalform N"],
+	   ("Rational.thy",["rational","simplification"],
+	    ["simplification","of_rationals"]))];
+Iterator 1;
+moveActiveRoot 1;
+autoCalculate 1 CompleteCalcHead;
+autoCalculate 1 (Step 1);
+appendFormula 1 "14";
+val ((pt,p),_) = get_calc 1; show_pt pt;
 
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+autoCalculate 1 (Step 1);
+val ((pt,p),_) = get_calc 1; show_pt pt;
+val Form res = (#1 o pt_extract) (pt, ([],Res));
+if p = ([], Res) andalso term2str res = "14" then ()
+else raise error "simplify.sml: append inform with final result ?!?";