1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Mon Jan 28 22:37:58 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Mon Jan 28 23:56:13 2013 +0100
     1.3 @@ -1383,7 +1383,7 @@
     1.4    (map_wpulls ~~ (pickWP_assms_tacs ~~ set_naturalss)) 1;
     1.5  
     1.6  fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs
     1.7 -  {context = ctxt, prems = _} =
     1.8 +  {context = ctxt, prems = _: thm list} =
     1.9    let
    1.10      val n = length map_comps;
    1.11    in

     2.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Mon Jan 28 22:37:58 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Mon Jan 28 23:56:13 2013 +0100
     2.3 @@ -152,7 +152,7 @@
     2.4      val timer = time (timer "Extracted terms & thms");
     2.5  
     2.6      (* nonemptiness check *)
     2.7 -    fun new_wit X wit = subset (op =) (#I wit, (0 upto m - 1) @ map snd X);
     2.8 +    fun new_wit X (wit: nonemptiness_witness) = subset (op =) (#I wit, (0 upto m - 1) @ map snd X);
     2.9  
    2.10      val all = m upto m + n - 1;
    2.11