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