src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 54970 891141de5672
parent 54900 136fe16e726a
child 55342 1bd9e637ac9f
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
     1.3 @@ -52,7 +52,8 @@
     1.4    val name_of_ctr: term -> string
     1.5    val name_of_disc: term -> string
     1.6    val dest_ctr: Proof.context -> string -> term -> term * term list
     1.7 -  val dest_case: Proof.context -> string -> typ list -> term -> (term list * term list) option
     1.8 +  val dest_case: Proof.context -> string -> typ list -> term ->
     1.9 +    (ctr_sugar * term list * term list) option
    1.10  
    1.11    val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
    1.12      (((bool * (bool * bool)) * term list) * binding) *
    1.13 @@ -266,7 +267,7 @@
    1.14    (case Term.strip_comb t of
    1.15      (Const (c, _), args as _ :: _) =>
    1.16      (case ctr_sugar_of ctxt s of
    1.17 -      SOME {casex = Const (case_name, _), discs = discs0, selss = selss0, ...} =>
    1.18 +      SOME (ctr_sugar as {casex = Const (case_name, _), discs = discs0, selss = selss0, ...}) =>
    1.19        if case_name = c then
    1.20          let val n = length discs0 in
    1.21            if n < length args then
    1.22 @@ -278,7 +279,7 @@
    1.23                val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
    1.24                val branches' = map2 (curry Term.betapplys) branches branch_argss;
    1.25              in
    1.26 -              SOME (conds, branches')
    1.27 +              SOME (ctr_sugar, conds, branches')
    1.28              end
    1.29            else
    1.30              NONE