--- 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
--- 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;