src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
changeset 53923 7b43d22accc3
parent 53918 0fc622be0185
child 53925 9008c4806198
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 26 16:00:18 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 26 16:10:57 2013 +0200
     1.3 @@ -734,7 +734,7 @@
     1.4      val (defs, exclss') =
     1.5        co_build_defs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
     1.6  
     1.7 -    fun prove_excl_tac (c, c', a) =
     1.8 +    fun excl_tac (c, c', a) =
     1.9        if a orelse c = c' orelse sequential then SOME (K (mk_primcorec_assumption_tac lthy []))
    1.10        else if simple then SOME (K (auto_tac lthy))
    1.11        else NONE;
    1.12 @@ -745,7 +745,7 @@
    1.13  *)
    1.14  
    1.15      val exclss'' = exclss' |> map (map (fn (idx, t) =>
    1.16 -      (idx, (Option.map (Goal.prove lthy [] [] t) (prove_excl_tac idx), t))));
    1.17 +      (idx, (Option.map (Goal.prove lthy [] [] t) (excl_tac idx), t))));
    1.18      val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss'';
    1.19      val (obligation_idxss, obligationss) = exclss''
    1.20        |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))