# HG changeset patch
# User wenzelm
# Date 1005237867 -3600
# Node ID a2deb1c3cd9b33c41da6d4e6c7170045c3baf1ff
# Parent  a79681a01f41cfa5ace64d8b95d6167b237338d3
make SML/XL of NJ happy;

diff -r a79681a01f41 -r a2deb1c3cd9b src/Pure/Isar/induct_attrib.ML
--- a/src/Pure/Isar/induct_attrib.ML	Thu Nov 08 17:42:43 2001 +0100
+++ b/src/Pure/Isar/induct_attrib.ML	Thu Nov 08 17:44:27 2001 +0100
@@ -116,7 +116,7 @@
     ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
       (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
 
-  val print = print_all_rules Display.pretty_thm_sg;
+  fun print x = print_all_rules Display.pretty_thm_sg x;
 
   fun dest ((casesT, casesS), (inductT, inductS)) =
     {type_cases = NetRules.rules casesT,
@@ -138,7 +138,7 @@
   type T = GlobalInductArgs.T;
 
   fun init thy = GlobalInduct.get thy;
-  val print = print_all_rules ProofContext.pretty_thm;
+  fun print x = print_all_rules ProofContext.pretty_thm x;
 end;
 
 structure LocalInduct = ProofDataFun(LocalInductArgs);