--- 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)) =