# HG changeset patch
# User blanchet
# Date 1393847300 -3600
# Node ID 0a8200e314749f83e1bb30ca716c9107b0c1b915
# Parent  756275b550d9730107144a32b6fb9f9b0143e19c
compile

diff -r 756275b550d9 -r 0a8200e31474 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -523,7 +523,7 @@
     lthy =
   let
     val nn = length fpTs;
-    val fpTs = range_type (snd (strip_typeN nn (fastype_of (co_rec_of dtor_coiters))));
+    val fpT = range_type (snd (strip_typeN nn (fastype_of (co_rec_of dtor_coiters))));
 
     fun generate_coiter pre ((pfss, cqfsss), f_absTs) dtor_coiter =
       (mk_binding pre,