make SML/XL of NJ happy;
authorwenzelm
Thu, 08 Nov 2001 17:44:27 +0100
changeset 12102 a2deb1c3cd9b
parent 12101 a79681a01f41
child 12103 b9bba87e1d78
make SML/XL of NJ happy;
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);