1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 21 07:24:18 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 21 07:50:32 2013 +0200
     1.3 @@ -832,7 +832,7 @@
     1.4      |> K |> nth_map sel_no |> AList.map_entry (op =) ctr
     1.5    end;
     1.6  
     1.7 -fun add_primcorec simple seq fixes specs of_specs lthy =
     1.8 +fun add_primcorec_ursive maybe_tac seq fixes specs of_specs lthy =
     1.9    let
    1.10      val (bs, mxs) = map_split (apfst fst) fixes;
    1.11      val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes |> split_list;
    1.12 @@ -884,12 +884,8 @@
    1.13        build_codefs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
    1.14  
    1.15      fun excl_tac (c, c', a) =
    1.16 -      if a orelse c = c' orelse seq then
    1.17 -        SOME (K (HEADGOAL (mk_primcorec_assumption_tac lthy [])))
    1.18 -      else if simple then
    1.19 -        SOME (K (auto_tac lthy))
    1.20 -      else
    1.21 -        NONE;
    1.22 +      if a orelse c = c' orelse seq then SOME (K (HEADGOAL (mk_primcorec_assumption_tac lthy [])))
    1.23 +      else maybe_tac;
    1.24  
    1.25  (*
    1.26  val _ = tracing ("exclusiveness properties:\n    \<cdot> " ^
    1.27 @@ -897,9 +893,9 @@
    1.28  *)
    1.29  
    1.30      val exclss'' = exclss' |> map (map (fn (idx, t) =>
    1.31 -      (idx, (Option.map (Goal.prove lthy [] [] t |> Thm.close_derivation) (excl_tac idx), t))));
    1.32 +      (idx, (Option.map (Goal.prove lthy [] [] t #> Thm.close_derivation) (excl_tac idx), t))));
    1.33      val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss'';
    1.34 -    val (obligation_idxss, obligationss) = exclss''
    1.35 +    val (obligation_idxss, goalss) = exclss''
    1.36        |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
    1.37        |> split_list o map split_list;
    1.38  
    1.39 @@ -1119,28 +1115,16 @@
    1.40        end;
    1.41  
    1.42      fun after_qed thmss' = fold_map Local_Theory.define defs #-> prove thmss';
    1.43 -
    1.44 -    val _ = if not simple orelse forall null obligationss then () else
    1.45 -      primrec_error "need exclusiveness proofs - use primcorecursive instead of primcorec";
    1.46    in
    1.47 -    if simple then
    1.48 -      lthy'
    1.49 -      |> after_qed (map (fn [] => []) obligationss)
    1.50 -      |> pair NONE o SOME
    1.51 -    else
    1.52 -      lthy'
    1.53 -      |> Proof.theorem NONE after_qed obligationss
    1.54 -      |> Proof.refine (Method.primitive_text I)
    1.55 -      |> Seq.hd
    1.56 -      |> rpair NONE o SOME
    1.57 +    (goalss, after_qed, lthy')
    1.58    end;
    1.59  
    1.60 -fun add_primcorec_ursive_cmd simple seq (raw_fixes, raw_specs') lthy =
    1.61 +fun add_primcorec_ursive_cmd maybe_tac seq (raw_fixes, raw_specs') lthy =
    1.62    let
    1.63      val (raw_specs, of_specs) = split_list raw_specs' ||> map (Option.map (Syntax.read_term lthy));
    1.64      val ((fixes, specs), _) = Specification.read_spec raw_fixes raw_specs lthy;
    1.65    in
    1.66 -    add_primcorec simple seq fixes specs of_specs lthy
    1.67 +    add_primcorec_ursive maybe_tac seq fixes specs of_specs lthy
    1.68      handle ERROR str => primrec_error str
    1.69    end
    1.70    handle Primrec_Error (str, eqns) =>
    1.71 @@ -1149,7 +1133,16 @@
    1.72      else error ("primcorec error:\n  " ^ str ^ "\nin\n  " ^
    1.73        space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns));
    1.74  
    1.75 -val add_primcorecursive_cmd = (the o fst) ooo add_primcorec_ursive_cmd false;
    1.76 -val add_primcorec_cmd = (the o snd) ooo add_primcorec_ursive_cmd true;
    1.77 +val add_primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
    1.78 +  lthy
    1.79 +  |> Proof.theorem NONE after_qed goalss
    1.80 +  |> Proof.refine (Method.primitive_text I)
    1.81 +  |> Seq.hd) ooo add_primcorec_ursive_cmd NONE;
    1.82 +
    1.83 +val add_primcorec_cmd = (fn (goalss, after_qed, lthy) =>
    1.84 +  lthy
    1.85 +  |> after_qed (map (fn [] => []
    1.86 +      | _ => primrec_error "need exclusiveness proofs - use primcorecursive instead of primcorec")
    1.87 +    goalss)) ooo add_primcorec_ursive_cmd (SOME (fn {context = ctxt, ...} => auto_tac ctxt));
    1.88  
    1.89  end;