--- a/src/HOLCF/Tools/cont_consts.ML Mon Feb 15 15:50:41 2010 +0100
+++ b/src/HOLCF/Tools/cont_consts.ML Mon Feb 15 17:17:51 2010 +0100
@@ -53,19 +53,8 @@
declaration with the original name, type ...=>..., and the original mixfix
is generated and connected to the other declaration via some translation.
*)
-fun const_binding mx = Binding.name o Syntax.const_name mx o Binding.name_of;
-
-fun fix_mixfix (syn , T, mx as Infix p ) =
- (const_binding mx syn, T, InfixName (Binding.name_of syn, p))
- | fix_mixfix (syn , T, mx as Infixl p ) =
- (const_binding mx syn, T, InfixlName (Binding.name_of syn, p))
- | fix_mixfix (syn , T, mx as Infixr p ) =
- (const_binding mx syn, T, InfixrName (Binding.name_of syn, p))
- | fix_mixfix decl = decl;
-
-fun transform decl =
+fun transform (c, T, mx) =
let
- val (c, T, mx) = fix_mixfix decl;
val c1 = Binding.name_of c;
val c2 = "_cont_" ^ c1;
val n = Syntax.mixfix_args mx
@@ -78,9 +67,9 @@
fun is_contconst (_,_,NoSyn ) = false
| 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 mx (Binding.name_of c)));
+| is_contconst (c,T,mx ) =
+ cfun_arity T >= Syntax.mixfix_args mx
+ handle ERROR msg => cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c));
(* add_consts(_i) *)
@@ -94,6 +83,7 @@
thy
|> Sign.add_consts_i
(normal_decls @ map first transformed_decls @ map second transformed_decls)
+ (* FIXME authentic syntax *)
|> Sign.add_trrules_i (maps third transformed_decls)
end;