# HG changeset patch
# User blanchet
# Date 1348235609 -7200
# Node ID 3cb59fdd69a8ae84e20759ecb08261757b134405
# Parent  464812bef4d9b89240c435f0dbb039f00f2c0c69
tuning

diff -r 464812bef4d9 -r 3cb59fdd69a8 src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -76,9 +76,9 @@
 
 fun mk_undefined T = Const (@{const_name undefined}, T);
 
-fun mk_ctr Ts ctr =
-  let val Type (_, Ts0) = body_type (fastype_of ctr) in
-    Term.subst_atomic_types (Ts0 ~~ Ts) ctr
+fun mk_ctr Ts t =
+  let val Type (_, Ts0) = body_type (fastype_of t) in
+    Term.subst_atomic_types (Ts0 ~~ Ts) t
   end;
 
 fun mk_disc_or_sel Ts t =
@@ -90,7 +90,7 @@
     | Free (s, _) => s
     | _ => error "Cannot extract name of constructor");
 
-fun rap u t = betapply (t, u);
+fun rapp u t = betapply (t, u);
 
 fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
 
@@ -226,7 +226,8 @@
 
           fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr);
 
-          fun alternate_disc k = Term.lambda u (alternate_disc_lhs (K o rap u o disc_free) (3 - k));
+          fun alternate_disc k =
+            Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
 
           fun mk_default T t =
             let
@@ -306,11 +307,11 @@
           val discs = map (mk_disc_or_sel As) discs0;
           val selss = map (map (mk_disc_or_sel As)) selss0;
 
-          val udiscs = map (rap u) discs;
-          val uselss = map (map (rap u)) selss;
+          val udiscs = map (rapp u) discs;
+          val uselss = map (map (rapp u)) selss;
 
-          val vdiscs = map (rap v) discs;
-          val vselss = map (map (rap v)) selss;
+          val vdiscs = map (rapp v) discs;
+          val vselss = map (map (rapp v)) selss;
         in
           (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs,
            sel_defss, lthy')