# HG changeset patch
# User blanchet
# Date 1482323758 -3600
# Node ID 19bc22274cd9490ceb496953fc2d17aa0e4c98c3
# Parent  8d7cb22482e399357d7a758f5316804561e93365
export ML function (towards nonuniform datatypes)

diff -r 8d7cb22482e3 -r 19bc22274cd9 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Dec 21 12:49:15 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Dec 21 13:35:58 2016 +0100
@@ -28,6 +28,8 @@
   val mk_disc_transfer_tac: Proof.context -> thm -> thm -> thm list -> tactic
   val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
   val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
+  val mk_induct_discharge_prem_tac: Proof.context -> int -> int -> thm list -> thm list ->
+    thm list -> thm list -> int -> int -> int list -> tactic
   val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
     thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
   val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic