# 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