1.1 --- a/src/smltest/IsacKnowledge/atools.sml	Sat Aug 20 13:00:20 2005 +0200
     1.2 +++ b/src/smltest/IsacKnowledge/atools.sml	Sat Aug 20 13:00:20 2005 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  if occurs_in t t then "OK" else raise error "atools.sml: occurs_in x x -> f";
     1.5  
     1.6  val t = str2t "x occurs_in x";
     1.7 -val Some (str, t') = eval_occurs_in 0 0 t 0;
     1.8 +val Some (str, t') = eval_occurs_in 0 "Atools.occurs'_in" t 0;
     1.9  if (term2s t') = "x occurs_in x = True" then ()
    1.10  else raise error "atools.sml: x occurs_in x = True ???";
    1.11  

     2.1 --- a/src/smltest/Scripts/calculate.sml	Sat Aug 20 13:00:20 2005 +0200
     2.2 +++ b/src/smltest/Scripts/calculate.sml	Sat Aug 20 13:00:20 2005 +0200
     2.3 @@ -1,6 +1,8 @@
     2.4 -(* use"tests/calculate.sml";
     2.5 -   use"calculate.sml";
     2.6 -   *)
     2.7 +(* test calculation of values for function constants
     2.8 +   (c) Walther Neuper 2000
     2.9 +
    2.10 +use"~/proto2/isac/src/smltest/Scripts/calculate.sml";
    2.11 +*)
    2.12  
    2.13  " ================= calculate.sml: calculate_ ======================== ";
    2.14  " ================= calculate.sml: aus script ======================== ";
    2.15 @@ -181,7 +183,7 @@
    2.16   trace_rewrite:=true;
    2.17   val thy = Test.thy;
    2.18   val t = (term_of o the o (parse thy)) "(-4) / 2";
    2.19 - val Some (_,t) = eval_cancel "xxx" 111 t thy;
    2.20 + val Some (_,t) = eval_cancel "xxx" "HOL.divide" t thy;
    2.21   term2str t;
    2.22  "-4 / 2 = (-2)";
    2.23  (*-------------- but ... *)