src/HOL/BNF/Tools/bnf_gfp_tactics.ML
changeset 51070 6ca703425c01
parent 50058 bb1fadeba35e
child 51447 a19e973fa2cf
     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