--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 25 16:43:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 25 16:43:46 2013 +0200
@@ -42,6 +42,7 @@
val mk_disc_or_sel: typ list -> term -> term
val name_of_ctr: term -> string
val name_of_disc: term -> string
+ val dest_ctr: Proof.context -> string -> term -> term * term list
val dest_case: Proof.context -> string -> typ list -> term -> (term list * term list) option
val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
@@ -215,6 +216,18 @@
val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
+fun dest_ctr ctxt s t =
+ let
+ val (f, args) = Term.strip_comb t;
+ in
+ (case ctr_sugar_of ctxt s of
+ SOME {ctrs, ...} =>
+ (case find_first (can (fo_match ctxt f)) ctrs of
+ SOME f' => (f', args)
+ | NONE => raise Fail "dest_ctr")
+ | NONE => raise Fail "dest_ctr")
+ end;
+
fun dest_case ctxt s Ts t =
(case Term.strip_comb t of
(Const (c, _), args as _ :: _) =>