sml-050210b sml-050210b
authorwneuper
Thu, 10 Feb 2005 16:16:09 +0100
changeset 2076dfedb702220a
parent 2075 fb02d0163801
child 2077 f7b87610de16
sml-050210b
src/sml/systest/tacis.sml
     1.1 --- a/src/sml/systest/tacis.sml	Thu Feb 10 16:16:09 2005 +0100
     1.2 +++ b/src/sml/systest/tacis.sml	Thu Feb 10 16:16:09 2005 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4   fetchProposedTactic 1 (*'' in tacis*);
     1.5   val ((pt,p),tacis) = get_calc 1;
     1.6   val ip = get_pos 1 1;
     1.7 - val (Form f, tac, asms, safe) = pt_extract (pt, p);
     1.8 + val (Form f, tac, asms) = pt_extract (pt, p);
     1.9   if term2str f = "[x = 1]"andalso p = ([],Res) andalso ip = ([],Res)then()else 
    1.10   raise error "tacis.sml: diff.behav. in fetchProposedTactic autoCalculate";
    1.11  
    1.12 @@ -152,7 +152,7 @@
    1.13  
    1.14   val ((pt,p),tacis) = get_calc 1;
    1.15   val ip = get_pos 1 1;
    1.16 - val (Form f, tac, asms, safe) = pt_extract (pt, p);
    1.17 + val (Form f, tac, asms) = pt_extract (pt, p);
    1.18   if term2str f = "[x = 1]"andalso p = ([],Res) andalso ip = ([],Res)then()else 
    1.19   raise error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (4)"; 
    1.20