1.1 --- a/src/HOLCF/Tools/cont_consts.ML	Tue Apr 21 11:11:04 2009 -0700
     1.2 +++ b/src/HOLCF/Tools/cont_consts.ML	Tue Apr 21 15:57:08 2009 -0700
     1.3 @@ -8,8 +8,8 @@
     1.4  
     1.5  signature CONT_CONSTS =
     1.6  sig
     1.7 -  val add_consts: (bstring * string * mixfix) list -> theory -> theory
     1.8 -  val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
     1.9 +  val add_consts: (binding * string * mixfix) list -> theory -> theory
    1.10 +  val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
    1.11  end;
    1.12  
    1.13  structure ContConsts: CONT_CONSTS =
    1.14 @@ -49,20 +49,24 @@
    1.15     declaration with the original name, type ...=>..., and the original mixfix
    1.16     is generated and connected to the other declaration via some translation.
    1.17  *)
    1.18 -fun fix_mixfix (syn                     , T, mx as Infix           p ) =
    1.19 -               (Syntax.const_name mx syn, T,       InfixName (syn, p))
    1.20 -  | fix_mixfix (syn                     , T, mx as Infixl           p ) =
    1.21 -               (Syntax.const_name mx syn, T,       InfixlName (syn, p))
    1.22 -  | fix_mixfix (syn                     , T, mx as Infixr           p ) =
    1.23 -               (Syntax.const_name mx syn, T,       InfixrName (syn, p))
    1.24 +fun const_binding mx = Binding.name o Syntax.const_name mx o Binding.name_of;
    1.25 +
    1.26 +fun fix_mixfix (syn                 , T, mx as Infix           p ) =
    1.27 +               (const_binding mx syn, T,       InfixName (Binding.name_of syn, p))
    1.28 +  | fix_mixfix (syn                 , T, mx as Infixl           p ) =
    1.29 +               (const_binding mx syn, T,       InfixlName (Binding.name_of syn, p))
    1.30 +  | fix_mixfix (syn                 , T, mx as Infixr           p ) =
    1.31 +               (const_binding mx syn, T,       InfixrName (Binding.name_of syn, p))
    1.32    | fix_mixfix decl = decl;
    1.33 +
    1.34  fun transform decl = let
    1.35          val (c, T, mx) = fix_mixfix decl;
    1.36 -        val c2 = "_cont_" ^ c;
    1.37 +        val c1 = Binding.name_of c;
    1.38 +        val c2 = "_cont_" ^ c1;
    1.39          val n  = Syntax.mixfix_args mx
    1.40 -    in     ((c ,               T,NoSyn),
    1.41 -            (c2,change_arrow n T,mx   ),
    1.42 -            trans_rules c2 c n mx) end;
    1.43 +    in     ((c, T, NoSyn),
    1.44 +            (Binding.name c2, change_arrow n T, mx),
    1.45 +            trans_rules c2 c1 n mx) end;
    1.46  
    1.47  fun cfun_arity (Type(n,[_,T])) = if n = @{type_name "->"} then 1+cfun_arity T else 0
    1.48  |   cfun_arity _               = 0;
    1.49 @@ -71,7 +75,7 @@
    1.50  |   is_contconst (_,_,Binder _) = false
    1.51  |   is_contconst (c,T,mx      ) = cfun_arity T >= Syntax.mixfix_args mx
    1.52                           handle ERROR msg => cat_error msg ("in mixfix annotation for " ^
    1.53 -                                               quote (Syntax.const_name mx c));
    1.54 +                                               quote (Syntax.const_name mx (Binding.name_of c)));
    1.55  
    1.56  
    1.57  (* add_consts(_i) *)
    1.58 @@ -83,7 +87,7 @@
    1.59      val transformed_decls = map transform contconst_decls;
    1.60    in
    1.61      thy
    1.62 -    |> (Sign.add_consts_i o map (upd_first Binding.name))
    1.63 +    |> Sign.add_consts_i
    1.64        (normal_decls @ map first transformed_decls @ map second transformed_decls)
    1.65      |> Sign.add_trrules_i (maps third transformed_decls)
    1.66    end;
    1.67 @@ -98,7 +102,7 @@
    1.68  
    1.69  val _ =
    1.70    OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
    1.71 -    (Scan.repeat1 P.const >> (Toplevel.theory o add_consts));
    1.72 +    (Scan.repeat1 P.const_binding >> (Toplevel.theory o add_consts));
    1.73  
    1.74  end;
    1.75