# HG changeset patch
# User blanchet
# Date 1346925456 -7200
# Node ID 64764f0efe802ea12305eeee0b3c32d2f048f5c0
# Parent  592a81b4d41339fd604fb891d026c6c05b241f93
tuning

diff -r 592a81b4d413 -r 64764f0efe80 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 06 11:55:23 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 06 11:57:36 2012 +0200
@@ -44,13 +44,13 @@
 fun type_args_constrained_of (((cAs, _), _), _) = cAs;
 val type_args_of = map fst o type_args_constrained_of;
 fun type_binder_of (((_, b), _), _) = b;
-fun mixfix_of_typ ((_, mx), _) = mx;
+fun mixfix_of ((_, mx), _) = mx;
 fun ctr_specs_of (_, ctr_specs) = ctr_specs;
 
 fun disc_of (((disc, _), _), _) = disc;
 fun ctr_of (((_, ctr), _), _) = ctr;
 fun args_of ((_, args), _) = args;
-fun mixfix_of_ctr (_, mx) = mx;
+fun ctr_mixfix_of (_, mx) = mx;
 
 fun prepare_data prepare_typ gfp specs fake_lthy lthy =
   let
@@ -74,7 +74,7 @@
     val bs = map type_binder_of specs;
     val fp_Ts = map mk_T bs;
 
-    val mixfixes = map mixfix_of_typ specs;
+    val mixfixes = map mixfix_of specs;
 
     val _ = (case duplicates Binding.eq_name bs of [] => ()
       | b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b)));
@@ -84,7 +84,7 @@
     val disc_binderss = map (map disc_of) ctr_specss;
     val ctr_binderss = map (map ctr_of) ctr_specss;
     val ctr_argsss = map (map args_of) ctr_specss;
-    val ctr_mixfixess = map (map mixfix_of_ctr) ctr_specss;
+    val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss;
 
     val sel_bindersss = map (map (map fst)) ctr_argsss;
     val ctr_Tsss = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
@@ -278,7 +278,7 @@
   let
     val fake_thy = Theory.copy
       #> fold (fn spec => Sign.add_type lthy
-        (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of_typ spec)) specs;
+        (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of spec)) specs;
     val fake_lthy = Proof_Context.background_theory fake_thy lthy;
   in
     prepare_data Syntax.read_typ info specs fake_lthy lthy