# HG changeset patch
# User blanchet
# Date 1380094537 -7200
# Node ID a48d4bd3faaabfc3d5dbd4f71d930a77c2182b3d
# Parent  c7364dca96f253899b00f4cca381422f51113058
use case rather than sequence of ifs in expansion

diff -r c7364dca96f2 -r a48d4bd3faaa src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Wed Sep 25 08:43:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Wed Sep 25 09:35:37 2013 +0200
@@ -37,6 +37,7 @@
   val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
 
   val mk_ctr: typ list -> term -> term
+  val mk_case: typ list -> typ -> term -> term
   val mk_disc_or_sel: typ list -> term -> term
 
   val name_of_ctr: term -> string
@@ -160,14 +161,14 @@
     Term.subst_atomic_types (Ts0 ~~ Ts) t
   end;
 
-fun mk_disc_or_sel Ts t =
-  Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
-
 fun mk_case Ts T t =
   let val (Type (_, Ts0), body) = strip_type (fastype_of t) |>> List.last in
     Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) t
   end;
 
+fun mk_disc_or_sel Ts t =
+  Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
+
 fun name_of_const what t =
   (case head_of t of
     Const (s, _) => s
diff -r c7364dca96f2 -r a48d4bd3faaa src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 08:43:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 09:35:37 2013 +0200
@@ -300,17 +300,11 @@
     SOME fp_sugar =>
     let
       val T = Type (s, Ts);
-      val x = Bound 0;
-      val {ctrs = ctrs0, discs = discs0, selss = selss0, ...} = of_fp_sugar #ctr_sugars fp_sugar;
+      val {ctrs = ctrs0, casex = case0, ...} = of_fp_sugar #ctr_sugars fp_sugar;
       val ctrs = map (mk_ctr Ts) ctrs0;
-      val discs = map (mk_disc_or_sel Ts) discs0;
-      val selss = map (map (mk_disc_or_sel Ts)) selss0;
-      val xdiscs = map (rapp x) discs;
-      val xselss = map (map (rapp x)) selss;
-      val xsel_ctrs = map2 (curry Term.list_comb) ctrs xselss;
-      val xif = mk_IfN T xdiscs xsel_ctrs;
+      val casex = mk_case Ts T case0;
     in
-      Const (@{const_name Let}, T --> (T --> T) --> T) $ t $ Abs (Name.uu, T, xif)
+      list_comb (casex, ctrs) $ t
     end
   | NONE => raise Fail "expand_ctr_term");