diff -r 64e850c3da9e -r 1035c89b4c02 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Sun May 18 15:04:09 2008 +0200
@@ -120,7 +120,7 @@
     (*analyze the LHS of a case equation to get a constructor*)
     fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
       | const_of eqn = error ("Ill-formed case equation: " ^
-                              Sign.string_of_term thy eqn);
+                              Syntax.string_of_term_global thy eqn);
 
     val constructors =
         map (head_of o const_of o FOLogic.dest_Trueprop o