# HG changeset patch
# User blanchet
# Date 1380121068 -7200
# Node ID c54ebf9dbd34d0e809be9f3c465da3cd5e84c688
# Parent  27da6373a64f6fcc4bc7c2a0e0b99cca2a14c7f4
removed spurious recursion

diff -r 27da6373a64f -r c54ebf9dbd34 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 16:52:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 16:57:48 2013 +0200
@@ -371,10 +371,7 @@
   (case fastype_of1 (bound_Ts, t) of
     Type (s, Ts) =>
     massage_let_if_case ctxt has_call (fn bound_Ts => fn t =>
-      if can (dest_ctr ctxt s) t then
-        t
-      else
-        massage_let_if_case ctxt has_call (K I) bound_Ts (expand_ctr_term ctxt s Ts t)) bound_Ts t
+      if can (dest_ctr ctxt s) t then t else expand_ctr_term ctxt s Ts t) bound_Ts t
   | _ => raise Fail "expand_corec_code_rhs");
 
 fun massage_corec_code_rhs ctxt massage_ctr =