src/HOL/Nominal/nominal_primrec.ML

--- a/src/HOL/Nominal/nominal_primrec.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sun May 18 15:04:09 2008 +0200
@@ -27,7 +27,7 @@
 
 fun primrec_err s = error ("Nominal primrec definition error:\n" ^ s);
 fun primrec_eq_err thy s eq =
-  primrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq));
+  primrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
 
 
 (* preprocessing of equations *)