# HG changeset patch
# User wenzelm
# Date 969223810 -7200
# Node ID be4824b7505d9907afbda02f3975e9b5d1f2d70f
# Parent  4961c73b5f60771a3bd6b7fa0e9afc2eb1084873
made SML/NJ happy;

diff -r 4961c73b5f60 -r be4824b7505d 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);