made SML/NJ happy;
authorwenzelm
Sun, 17 Sep 2000 22:50:10 +0200
changeset 10013 be4824b7505d
parent 10012 4961c73b5f60
child 10014 d41ab495ab14
made SML/NJ happy;
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);