# HG changeset patch
# User blanchet
# Date 1379523429 -7200
# Node ID 9b034e6b977ce26ce82822708d1c8b0a32af87c1
# Parent  0643a443bb630fe211c064ef81636a3f7ff0d205
tuning (alphabetical order)

diff -r 0643a443bb63 -r 9b034e6b977c src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 18 18:56:48 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 18 18:57:09 2013 +0200
@@ -7,6 +7,7 @@
 
 signature BNF_FP_REC_SUGAR_TACTICS =
 sig
+  val mk_primcorec_assumption_tac: Proof.context -> tactic
   val mk_primcorec_code_tac: Proof.context -> thm -> thm list -> tactic
   val mk_primcorec_code_of_ctr_tac: Proof.context -> int list -> thm list -> tactic
   val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
@@ -14,7 +15,6 @@
     thm list list list -> thm list -> thm list -> thm list -> tactic
   val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     tactic
-  val mk_primcorec_assumption_tac: Proof.context -> tactic
   val mk_primrec_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> tactic
 end;