1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 17:36:02 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 17:52:01 2012 +0200
     1.3 @@ -72,15 +72,8 @@
     1.4  fun mk_sumEN_balanced 1 = @{thm one_pointE}
     1.5    | mk_sumEN_balanced 2 = @{thm sumE} (*optimization*)
     1.6    | mk_sumEN_balanced n =
     1.7 -    let
     1.8 -      val thm =
     1.9 -        Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
    1.10 -          (replicate n asm_rl) OF (replicate n (impI RS allI));
    1.11 -      val f as (_, f_T) =
    1.12 -        Term.add_vars (prop_of thm) []
    1.13 -        |> filter (fn ((s, _), _) => s = "f") |> the_single;
    1.14 -      val inst = [pairself (cterm_of @{theory}) (Var f, Abs (Name.uu, domain_type f_T, Bound 0))];
    1.15 -    in cterm_instantiate inst thm end;
    1.16 +    Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
    1.17 +      (replicate n asm_rl) OF (replicate n (impI RS allI)) RS @{thm obj_one_pointE};
    1.18  
    1.19  fun tick v f = Term.lambda v (HOLogic.mk_prod (v, f $ v));
    1.20