# HG changeset patch
# User traytel
# Date 1359413773 -3600
# Node ID 6ca703425c015fbf1393f9d247320bea32037403
# Parent  2f50ddd3b5860b830d65cb6e81c83d79c8204c98
made SML/NJ happy

diff -r 2f50ddd3b586 -r 6ca703425c01 src/HOL/BNF/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Mon Jan 28 22:37:58 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Mon Jan 28 23:56:13 2013 +0100
@@ -1383,7 +1383,7 @@
   (map_wpulls ~~ (pickWP_assms_tacs ~~ set_naturalss)) 1;
 
 fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs
-  {context = ctxt, prems = _} =
+  {context = ctxt, prems = _: thm list} =
   let
     val n = length map_comps;
   in
diff -r 2f50ddd3b586 -r 6ca703425c01 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Mon Jan 28 22:37:58 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Mon Jan 28 23:56:13 2013 +0100
@@ -152,7 +152,7 @@
     val timer = time (timer "Extracted terms & thms");
 
     (* nonemptiness check *)
-    fun new_wit X wit = subset (op =) (#I wit, (0 upto m - 1) @ map snd X);
+    fun new_wit X (wit: nonemptiness_witness) = subset (op =) (#I wit, (0 upto m - 1) @ map snd X);
 
     val all = m upto m + n - 1;