src/HOL/Tools/induct_method.ML

--- a/src/HOL/Tools/induct_method.ML	Sun Sep 17 22:25:18 2000 +0200
+++ b/src/HOL/Tools/induct_method.ML	Sun Sep 17 22:50:10 2000 +0200
@@ -93,7 +93,7 @@
   type T = GlobalInductArgs.T;
 
   fun init thy = GlobalInduct.get thy;
-  val print = GlobalInductArgs.print o ProofContext.sign_of;
+  fun print x = GlobalInductArgs.print (ProofContext.sign_of x);
 end;
 
 structure LocalInduct = ProofDataFun(LocalInductArgs);