1.1 --- a/test/Tools/isac/Interpret/script.sml	Fri Mar 04 11:30:37 2011 +0100
     1.2 +++ b/test/Tools/isac/Interpret/script.sml	Fri Mar 04 11:43:45 2011 +0100
     1.3 @@ -177,7 +177,7 @@
     1.4  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
     1.5  trace_rewrite:=false;
     1.6  (*Exception TYPE raised:
     1.7 -Illegal type for constant "op =" :: "[real, bool] => bool"
     1.8 +Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
     1.9  Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
    1.10  ListG.nth_ (1 + -1 + -1) []
    1.11  Exception-
    1.12 @@ -185,7 +185,7 @@
    1.13        ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
    1.14           [],
    1.15           [Const ("Trueprop", "bool => prop") $
    1.16 -               (Const ("op =", "[RealDef.real, bool] => bool") $ ... $ ...)])
    1.17 +               (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
    1.18     raised
    1.19  ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
    1.20  ie. the argument had not been simplified before          ^^^^^^^^^^^^^^^