1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 18 18:56:48 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 18 18:57:09 2013 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  signature BNF_FP_REC_SUGAR_TACTICS =
     1.6  sig
     1.7 +  val mk_primcorec_assumption_tac: Proof.context -> tactic
     1.8    val mk_primcorec_code_tac: Proof.context -> thm -> thm list -> tactic
     1.9    val mk_primcorec_code_of_ctr_tac: Proof.context -> int list -> thm list -> tactic
    1.10    val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
    1.11 @@ -14,7 +15,6 @@
    1.12      thm list list list -> thm list -> thm list -> thm list -> tactic
    1.13    val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
    1.14      tactic
    1.15 -  val mk_primcorec_assumption_tac: Proof.context -> tactic
    1.16    val mk_primrec_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> tactic
    1.17  end;
    1.18