# HG changeset patch
# User blanchet
# Date 1380303049 -7200
# Node ID 949cef2095e236f368daea670ea1af4819b0ba1f
# Parent  024fadbd03f02ee4f60d412f56221078debb8cc3
faster exit in common case

diff -r 024fadbd03f0 -r 949cef2095e2 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Sep 27 17:57:45 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Sep 27 19:30:49 2013 +0200
@@ -368,8 +368,10 @@
           | _ => ill_formed_corec_call ctxt t)
         else
           build_map_Inl (T, U) $ t) bound_Ts;
+
+    val T = fastype_of1 (bound_Ts, t);
   in
-    massage_call bound_Ts U (fastype_of1 (bound_Ts, t)) t
+    if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t
   end;
 
 fun expand_ctr_term ctxt s Ts t =