diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Library/Eval_Witness.thy	Sun May 18 15:04:09 2008 +0200
@@ -51,7 +51,7 @@
   fun check_type T = 
     if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"])
     then T
-    else error ("Type " ^ quote (Sign.string_of_typ thy T) ^ " not allowed for ML witnesses")
+    else error ("Type " ^ quote (Syntax.string_of_typ_global thy T) ^ " not allowed for ML witnesses")
 
   fun dest_exs  0 t = t
     | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) =