# HG changeset patch
# User blanchet
# Date 1389361177 -3600
# Node ID 891141de56721186b379fc5a25d6ebfe9222f2e5
# Parent  0ac0b6576d21a5b695a608d653295844d991ac56
only destruct cases equipped with the right stuff (in particular, 'sel_split')

diff -r 0ac0b6576d21 -r 891141de5672 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
@@ -158,10 +158,10 @@
             (case fastype_of1 (bound_Ts, nth args n) of
               Type (s, Ts) =>
               (case dest_case ctxt s Ts t of
-                NONE => apsnd (f conds t)
-              | SOME (conds', branches) =>
-                apfst (cons s) o fold_rev (uncurry fld)
-                  (map (append conds o conjuncts_s) conds' ~~ branches))
+                SOME (ctr_sugar as {sel_splits = _ :: _, ...}, conds', branches) =>
+                apfst (cons ctr_sugar) o fold_rev (uncurry fld)
+                  (map (append conds o conjuncts_s) conds' ~~ branches)
+              | _ => apsnd (f conds t))
             | _ => apsnd (f conds t))
           else
             apsnd (f conds t)
@@ -171,7 +171,10 @@
     fld [] t o pair []
   end;
 
-fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex);
+fun case_of ctxt s =
+  (case ctr_sugar_of ctxt s of
+    SOME {casex = Const (s', _), sel_splits = _ :: _, ...} => SOME s'
+  | _ => NONE);
 
 fun massage_let_if_case ctxt has_call massage_leaf =
   let
@@ -319,8 +322,6 @@
     if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t
   end;
 
-val fold_rev_corec_call = fold_rev_let_if_case;
-
 fun expand_to_ctr_term ctxt s Ts t =
   (case ctr_sugar_of ctxt s of
     SOME {ctrs, casex, ...} =>
@@ -342,10 +343,7 @@
   snd ooo fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb);
 
 fun case_thms_of_term ctxt bound_Ts t =
-  let
-    val (caseT_names, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t ();
-    val ctr_sugars = map (the o ctr_sugar_of ctxt) caseT_names;
-  in
+  let val (ctr_sugars, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t () in
     (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #sel_splits ctr_sugars,
      maps #sel_split_asms ctr_sugars)
   end;
@@ -876,7 +874,7 @@
   let
     val sel_no = find_first (curry (op =) ctr o #ctr) basic_ctr_specs
       |> find_index (curry (op =) sel) o #sels o the;
-    fun find t = if has_call t then snd (fold_rev_corec_call ctxt (K cons) [] t []) else [];
+    fun find t = if has_call t then snd (fold_rev_let_if_case ctxt (K cons) [] t []) else [];
   in
     find rhs_term
     |> K |> nth_map sel_no |> AList.map_entry (op =) ctr
diff -r 0ac0b6576d21 -r 891141de5672 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
@@ -52,7 +52,8 @@
   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 dest_case: Proof.context -> string -> typ list -> term ->
+    (ctr_sugar * term list * term list) option
 
   val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     (((bool * (bool * bool)) * term list) * binding) *
@@ -266,7 +267,7 @@
   (case Term.strip_comb t of
     (Const (c, _), args as _ :: _) =>
     (case ctr_sugar_of ctxt s of
-      SOME {casex = Const (case_name, _), discs = discs0, selss = selss0, ...} =>
+      SOME (ctr_sugar as {casex = Const (case_name, _), discs = discs0, selss = selss0, ...}) =>
       if case_name = c then
         let val n = length discs0 in
           if n < length args then
@@ -278,7 +279,7 @@
               val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
               val branches' = map2 (curry Term.betapplys) branches branch_argss;
             in
-              SOME (conds, branches')
+              SOME (ctr_sugar, conds, branches')
             end
           else
             NONE