# HG changeset patch
# User blanchet
# Date 1347291362 -7200
# Node ID 4bf74375b4f737d842e6c8ce2b98cc2568286684
# Parent  0dc6cf758ed1b348b81f780487307e79d1e19e63
fixed base case of "mk_sumEN_balanced"

diff -r 0dc6cf758ed1 -r 4bf74375b4f7 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 17:36:02 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 17:36:02 2012 +0200
@@ -69,16 +69,18 @@
 
 val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case;
 
-fun mk_sumEN_balanced n =
-  let
-    val thm =
-      Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
-        (replicate n asm_rl) OF (replicate n (impI RS allI));
-    val f as (_, f_T) =
-      Term.add_vars (prop_of thm) []
-      |> filter (fn ((s, _), _) => s = "f") |> the_single;
-    val inst = [pairself (cterm_of @{theory}) (Var f, Abs (Name.uu, domain_type f_T, Bound 0))];
-  in cterm_instantiate inst thm end;
+fun mk_sumEN_balanced 1 = @{thm one_pointE}
+  | mk_sumEN_balanced 2 = @{thm sumE} (*optimization*)
+  | mk_sumEN_balanced n =
+    let
+      val thm =
+        Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
+          (replicate n asm_rl) OF (replicate n (impI RS allI));
+      val f as (_, f_T) =
+        Term.add_vars (prop_of thm) []
+        |> filter (fn ((s, _), _) => s = "f") |> the_single;
+      val inst = [pairself (cterm_of @{theory}) (Var f, Abs (Name.uu, domain_type f_T, Bound 0))];
+    in cterm_instantiate inst thm end;
 
 fun tick v f = Term.lambda v (HOLogic.mk_prod (v, f $ v));