diff -r d236572c99f2 -r 32d7766945fb test/Tools/isac/Interpret/script.sml
--- a/test/Tools/isac/Interpret/script.sml	Fri Mar 04 11:30:37 2011 +0100
+++ b/test/Tools/isac/Interpret/script.sml	Fri Mar 04 11:43:45 2011 +0100
@@ -177,7 +177,7 @@
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
 trace_rewrite:=false;
 (*Exception TYPE raised:
-Illegal type for constant "op =" :: "[real, bool] => bool"
+Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
 Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
 ListG.nth_ (1 + -1 + -1) []
 Exception-
@@ -185,7 +185,7 @@
       ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
          [],
          [Const ("Trueprop", "bool => prop") $
-               (Const ("op =", "[RealDef.real, bool] => bool") $ ... $ ...)])
+               (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
    raised
 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
 ie. the argument had not been simplified before          ^^^^^^^^^^^^^^^