--- a/src/HOLCF/Tools/cont_consts.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOLCF/Tools/cont_consts.ML Sat Mar 07 22:17:25 2009 +0100
@@ -52,11 +52,11 @@
is generated and connected to the other declaration via some translation.
*)
fun fix_mixfix (syn , T, mx as Infix p ) =
- (Syntax.const_name syn mx, T, InfixName (syn, p))
+ (Syntax.const_name mx syn, T, InfixName (syn, p))
| fix_mixfix (syn , T, mx as Infixl p ) =
- (Syntax.const_name syn mx, T, InfixlName (syn, p))
+ (Syntax.const_name mx syn, T, InfixlName (syn, p))
| fix_mixfix (syn , T, mx as Infixr p ) =
- (Syntax.const_name syn mx, T, InfixrName (syn, p))
+ (Syntax.const_name mx syn, T, InfixrName (syn, p))
| fix_mixfix decl = decl;
fun transform decl = let
val (c, T, mx) = fix_mixfix decl;
@@ -73,7 +73,7 @@
| is_contconst (_,_,Binder _) = false
| is_contconst (c,T,mx ) = cfun_arity T >= Syntax.mixfix_args mx
handle ERROR msg => cat_error msg ("in mixfix annotation for " ^
- quote (Syntax.const_name c mx));
+ quote (Syntax.const_name mx c));
(* add_consts(_i) *)
@@ -85,10 +85,9 @@
val transformed_decls = map transform contconst_decls;
in
thy
- |> Sign.add_consts_i normal_decls
- |> Sign.add_consts_i (map first transformed_decls)
- |> Sign.add_syntax_i (map second transformed_decls)
- |> Sign.add_trrules_i (List.concat (map third transformed_decls))
+ |> (Sign.add_consts_i o map (upd_first Binding.name))
+ (normal_decls @ map first transformed_decls @ map second transformed_decls)
+ |> Sign.add_trrules_i (maps third transformed_decls)
end;
val add_consts = gen_add_consts Syntax.read_typ_global;