# HG changeset patch
# User haftmann
# Date 1178785337 -7200
# Node ID 475ff421a6a34b214815a323788a5a8570aa6485
# Parent  0dbcb73bf9bf9f7c280584c8b70da78826eb2620
consts in consts_code Isar commands are now referred to by usual term syntax

diff -r 0dbcb73bf9bf -r 475ff421a6a3 NEWS
--- a/NEWS	Thu May 10 10:21:50 2007 +0200
+++ b/NEWS	Thu May 10 10:22:17 2007 +0200
@@ -68,20 +68,23 @@
 
 *** Pure ***
 
+* code generator: consts in 'consts_code' Isar commands are now referred
+  to by usual term syntax (including optional type annotations).
+
 * code generator: 
-  - Isar "definition"s and primitive instance definitions are added explicitly
-    to the table of defining equations
+  - Isar 'definition's, 'constdef's and primitive instance definitions are added
+    explicitly to the table of defining equations
   - primitive definitions are not used as defining equations by default any longer
   - defining equations are now definitly restricted to meta "==" and object
         equality "="
   - HOL theories have been adopted accordingly
 
 * class_package.ML offers a combination of axclasses and locales to
-achieve Haskell-like type classes in Isabelle. See
+achieve Haskell-like type classes in Isabelle.  See
 HOL/ex/Classpackage.thy for examples.
 
 * Yet another code generator framework allows to generate executable
-code for ML and Haskell (including "class"es). A short usage sketch:
+code for ML and Haskell (including "class"es).  A short usage sketch:
 
     internal compilation:
         code_gen <list of constants (term syntax)> (SML #)
diff -r 0dbcb73bf9bf -r 475ff421a6a3 doc-src/HOL/HOL.tex
--- a/doc-src/HOL/HOL.tex	Thu May 10 10:21:50 2007 +0200
+++ b/doc-src/HOL/HOL.tex	Thu May 10 10:22:17 2007 +0200
@@ -1441,7 +1441,12 @@
 If the formula involves explicit quantifiers, \texttt{arith_tac} may take
 super-exponential time and space.
 
-If \texttt{arith_tac} fails, try to find relevant arithmetic results in
the library.  The theories \texttt{Nat} and \texttt{NatArith} contain
theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.
Theory \texttt{Divides} contains theorems about \texttt{div} and
\texttt{mod}.  Use Proof General's \emph{find} button (or other search
facilities) to locate them.
+If \texttt{arith_tac} fails, try to find relevant arithmetic results in
+the library.  The theories \texttt{Nat} and \texttt{NatArith} contain
+theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.
+Theory \texttt{Divides} contains theorems about \texttt{div} and
+\texttt{mod}.  Use Proof General's \emph{find} button (or other search
+facilities) to locate them.
 
 \index{nat@{\textit{nat}} type|)}
 
@@ -2793,12 +2798,14 @@
 \begin{rail}
 constscode : 'consts_code' (codespec +);
 
-codespec : name ( '::' type) ? template attachment ?;
+codespec : const template attachment ?;
 
 typescode : 'types_code' (tycodespec +);
 
 tycodespec : name template attachment ?;
 
+const : term;
+
 template: '(' string ')';
 
 attachment: 'attach' modespec ? verblbrace text verbrbrace;
@@ -2859,8 +2866,8 @@
 are immediately executable, may be associated with a piece of ML
 code manually using the \ttindex{consts_code} command
 (see Fig.~\ref{fig:HOL:codegen-configuration}).
-It takes a list whose elements consist of a constant name, together
-with an optional type constraint (to account for overloading), and a
+It takes a list whose elements consist of a constant (given in usual term syntax
+-- an explicit type constraint accounts for overloading), and a
 mixfix template describing the ML code. The latter is very much the
 same as the mixfix templates used when declaring new constants.
 The most notable difference is that terms may be included in the ML
diff -r 0dbcb73bf9bf -r 475ff421a6a3 doc-src/IsarRef/logics.tex
--- a/doc-src/IsarRef/logics.tex	Thu May 10 10:21:50 2007 +0200
+++ b/doc-src/IsarRef/logics.tex	Thu May 10 10:22:17 2007 +0200
@@ -730,12 +730,14 @@
 
 'consts\_code' (codespec +);
 
-codespec : name ( '::' type) ? template attachment ?;
+codespec : const template attachment ?;
 
 'types\_code' (tycodespec +);
 
 tycodespec : name template attachment ?;
 
+const: term;
+
 template: '(' string ')';
 
 attachment: 'attach' modespec ? verblbrace text verbrbrace;
diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Thu May 10 10:21:50 2007 +0200
+++ b/src/HOL/Code_Generator.thy	Thu May 10 10:22:17 2007 +0200
@@ -39,7 +39,7 @@
   "Not"     ("not")
   "op |"    ("(_ orelse/ _)")
   "op &"    ("(_ andalso/ _)")
-  "HOL.If"      ("(if _/ then _/ else _)")
+  "If"      ("(if _/ then _/ else _)")
 
 setup {*
 let
diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Thu May 10 10:21:50 2007 +0200
+++ b/src/HOL/Extraction/Higman.thy	Thu May 10 10:22:17 2007 +0200
@@ -333,8 +333,8 @@
 *}
 
 consts_code
-  arbitrary :: "LT"  ("({* L0 [] [] *})")
-  arbitrary :: "TT"  ("({* T0 A [] [] [] R0 *})")
+  "arbitrary :: LT"  ("({* L0 [] [] *})")
+  "arbitrary :: TT"  ("({* T0 A [] [] [] R0 *})")
 
 code_module Higman
 contains
diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/HOL/Extraction/Pigeonhole.thy
--- a/src/HOL/Extraction/Pigeonhole.thy	Thu May 10 10:21:50 2007 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy	Thu May 10 10:22:17 2007 +0200
@@ -293,7 +293,7 @@
 
 
 consts_code
-  arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}")
+  "arbitrary :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")
 
 definition
   arbitrary_nat_pair :: "nat \<times> nat" where
diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/HOL/Integ/Numeral.thy
--- a/src/HOL/Integ/Numeral.thy	Thu May 10 10:21:50 2007 +0200
+++ b/src/HOL/Integ/Numeral.thy	Thu May 10 10:22:17 2007 +0200
@@ -667,18 +667,17 @@
 *}
 
 consts_code
-  "HOL.zero" :: "int"                ("0")
-  "HOL.one" :: "int"                 ("1")
-  "HOL.uminus" :: "int => int"       ("~")
-  "HOL.plus" :: "int => int => int"  ("(_ +/ _)")
-  "HOL.times" :: "int => int => int" ("(_ */ _)")
-  "Orderings.less" :: "int => int => bool" ("(_ </ _)")
-  "Orderings.less_eq" :: "int => int => bool" ("(_ <=/ _)")
-  "neg"                              ("(_ < 0)")
+  "0 :: int"                   ("0")
+  "1 :: int"                   ("1")
+  "uminus :: int => int"       ("~")
+  "op + :: int => int => int"  ("(_ +/ _)")
+  "op * :: int => int => int"  ("(_ */ _)")
+  "op \<le> :: int => int => bool" ("(_ <=/ _)")
+  "op < :: int => int => bool" ("(_ </ _)")
 
 quickcheck_params [default_type = int]
 
-(* setup continues in theory Presburger *)
+(*setup continues in theory Presburger*)
 
 hide (open) const Pls Min B0 B1 succ pred
 
diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Thu May 10 10:21:50 2007 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Thu May 10 10:22:17 2007 +0200
@@ -488,8 +488,8 @@
 subsection {* Generating executable code *}
 
 consts_code
-  arbitrary :: "'a"       ("(error \"arbitrary\")")
-  arbitrary :: "'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
+  "arbitrary :: 'a"       ("(error \"arbitrary\")")
+  "arbitrary :: 'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
 
 code_module Norm
 contains
diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Thu May 10 10:21:50 2007 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Thu May 10 10:22:17 2007 +0200
@@ -170,7 +170,7 @@
 *}
 
 consts_code
-  "HOL.zero" :: nat ("0")
+  "0 \<Colon> nat" ("0")
   Suc ("(_ + 1)")
 
 text {*
diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Thu May 10 10:21:50 2007 +0200
+++ b/src/HOL/Library/ExecutableRat.thy	Thu May 10 10:22:17 2007 +0200
@@ -140,13 +140,13 @@
 consts_code
   div_zero ("(raise/ (Fail/ \"Division by zero\"))")
   Fract ("({*erat_of_quotient*} (_) (_))")
-  HOL.zero :: rat ("({*Rat True 0 1*})")
-  HOL.one :: rat ("({*Rat True 1 1*})")
-  HOL.plus :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
-  HOL.uminus :: "rat \<Rightarrow> rat" ("({*uminus \<Colon> erat \<Rightarrow> erat*} (_))")
-  HOL.times :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
-  HOL.inverse :: "rat \<Rightarrow> rat" ("({*inverse \<Colon> erat \<Rightarrow> erat*} (_))")
-  Orderings.less_eq :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
-  "op =" :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
+  "0 \<Colon> rat" ("({*Rat True 0 1*})")
+  "1 \<Colon> rat" ("({*Rat True 1 1*})")
+  "plus \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
+  "uminus \<Colon> rat \<Rightarrow> rat" ("({*uminus \<Colon> erat \<Rightarrow> erat*} (_))")
+  "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
+  "inverse \<Colon> rat \<Rightarrow> rat" ("({*inverse \<Colon> erat \<Rightarrow> erat*} (_))")
+  "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
+  "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
 
 end
diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Thu May 10 10:21:50 2007 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Thu May 10 10:22:17 2007 +0200
@@ -343,19 +343,18 @@
 subsubsection {* const serializations *}
 
 consts_code
-  "{}"      ("[]")
-  "insert"  ("{*insertl*}")
-  "op Un"   ("{*unionl*}")
-  "op Int"  ("{*intersect*}")
-  "minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
-            ("{*flip subtract*}")
-  "image"   ("{*map_distinct*}")
-  "Union"   ("{*unions*}")
-  "Inter"   ("{*intersects*}")
-  "UNION"   ("{*map_union*}")
-  "INTER"   ("{*map_inter*}")
-  "Ball"    ("{*Blall*}")
-  "Bex"     ("{*Blex*}")
-  "filter_set" ("{*filter*}")
+  "{}" ("{*[]*}")
+  insert ("{*insertl*}")
+  "op \<union>" ("{*unionl*}")
+  "op \<inter>" ("{*intersect*}")
+  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
+  image ("{*map_distinct*}")
+  Union ("{*unions*}")
+  Inter ("{*intersects*}")
+  UNION ("{*map_union*}")
+  INTER ("{*map_inter*}")
+  Ball ("{*Blall*}")
+  Bex ("{*Blex*}")
+  filter_set ("{*filter*}")
 
 end
diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Thu May 10 10:21:50 2007 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Thu May 10 10:22:17 2007 +0200
@@ -73,8 +73,8 @@
 *}
 
   "arbitrary" ("(raise Match)")
-  "arbitrary" :: "val" ("{* Unit *}")
-  "arbitrary" :: "cname" ("\"\"")
+  "arbitrary :: val" ("{* Unit *}")
+  "arbitrary :: cname" ("\"\"")
 
   "Object" ("\"Object\"")
   "list_name" ("\"list\"")
diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Thu May 10 10:21:50 2007 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Thu May 10 10:22:17 2007 +0200
@@ -102,8 +102,8 @@
 *}
 
   "arbitrary" ("(raise Match)")
-  "arbitrary" :: "val" ("{* Unit *}")
-  "arbitrary" :: "cname" ("{* Object *}")
+  "arbitrary :: val" ("{* Unit *}")
+  "arbitrary :: cname" ("{* Object *}")
 
   "list_nam" ("\"list\"")
   "test_nam" ("\"test\"")
diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Thu May 10 10:21:50 2007 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Thu May 10 10:22:17 2007 +0200
@@ -285,12 +285,12 @@
    (c as Const (s, T), ts) =>
      (case DatatypePackage.datatype_of_case thy s of
         SOME {index, descr, ...} =>
-          if is_some (get_assoc_code thy s T) then NONE else
+          if is_some (get_assoc_code thy (s, T)) then NONE else
           SOME (pretty_case thy defs gr dep module brack
             (#3 (the (AList.lookup op = descr index))) c ts)
       | NONE => case (DatatypePackage.datatype_of_constr thy s, strip_type T) of
         (SOME {index, descr, ...}, (_, U as Type _)) =>
-          if is_some (get_assoc_code thy s T) then NONE else
+          if is_some (get_assoc_code thy (s, T)) then NONE else
           let val SOME args = AList.lookup op =
             (#3 (the (AList.lookup op = descr index))) s
           in
@@ -305,7 +305,7 @@
       (case DatatypePackage.get_datatype thy s of
          NONE => NONE
        | SOME {descr, ...} =>
-           if isSome (get_assoc_type thy s) then NONE else
+           if is_some (get_assoc_type thy s) then NONE else
            let
              val (gr', ps) = foldl_map
                (invoke_tycodegen thy defs dep module false) (gr, Ts);
diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Thu May 10 10:21:50 2007 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu May 10 10:22:17 2007 +0200
@@ -617,7 +617,7 @@
 
 fun inductive_codegen thy defs gr dep module brack t = (case strip_comb t of
     (Const ("Collect", Type (_, [_, Type (_, [U])])), [u]) => (case strip_comb u of
-        (Const (s, T), ts) => (case (get_clauses thy s, get_assoc_code thy s T) of
+        (Const (s, T), ts) => (case (get_clauses thy s, get_assoc_code thy (s, T)) of
           (SOME (names, thyname, k, intrs), NONE) =>
             let val (gr', call_p) = mk_ind_call thy defs gr dep module true
               s T (ts @ [Term.dummy_pattern U]) names thyname k intrs
@@ -628,7 +628,7 @@
         | _ => NONE)
       | _ => NONE)
   | (Const (s, T), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy)) s of
-      NONE => (case (get_clauses thy s, get_assoc_code thy s T) of
+      NONE => (case (get_clauses thy s, get_assoc_code thy (s, T)) of
         (SOME (names, thyname, k, intrs), NONE) =>
           if length ts < k then NONE else SOME
             (let val (gr', call_p) = mk_ind_call thy defs gr dep module false
diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Thu May 10 10:21:50 2007 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Thu May 10 10:22:17 2007 +0200
@@ -151,7 +151,7 @@
   end;
 
 fun recfun_codegen thy defs gr dep module brack t = (case strip_comb t of
-    (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy s T) of
+    (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy (s, T)) of
        (([], _), _) => NONE
      | (_, SOME _) => NONE
      | ((eqns, thyname), NONE) =>
diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/Pure/Tools/codegen_consts.ML
--- a/src/Pure/Tools/codegen_consts.ML	Thu May 10 10:21:50 2007 +0200
+++ b/src/Pure/Tools/codegen_consts.ML	Thu May 10 10:22:17 2007 +0200
@@ -8,13 +8,14 @@
 
 signature CODEGEN_CONSTS =
 sig
-  type const = string * string option (* constant name, possibly instance *)
+  type const = string * string option (*constant name, possibly instance*)
   val const_ord: const * const -> order
   val eq_const: const * const -> bool
   structure Consttab: TABLE
   val const_of_cexpr: theory -> string * typ -> const
   val string_of_typ: theory -> typ -> string
   val string_of_const: theory -> const -> string
+  val read_bare_const: theory -> string -> string * typ
   val read_const: theory -> string -> const
   val read_const_exprs: theory -> (const list -> const list)
     -> string list -> const list
@@ -72,14 +73,16 @@
 
 (* reading constants as terms and wildcards pattern *)
 
-fun read_const thy raw_t =
+fun read_bare_const thy raw_t =
   let
     val t = Sign.read_term thy raw_t;
   in case try dest_Const t
-   of SOME c_ty => const_of_cexpr thy c_ty
+   of SOME c_ty => c_ty
     | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
   end;
 
+fun read_const thy = const_of_cexpr thy o read_bare_const thy;
+
 local
 
 fun consts_of thy some_thyname =
diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu May 10 10:21:50 2007 +0200
+++ b/src/Pure/codegen.ML	Thu May 10 10:22:17 2007 +0200
@@ -35,13 +35,13 @@
     (string * string) list * codegr
   val generate_code_i: theory -> string list -> string -> (string * term) list ->
     (string * string) list * codegr
-  val assoc_consts: (xstring * string option * (term mixfix list *
-    (string * string) list)) list -> theory -> theory
-  val assoc_consts_i: (xstring * typ option * (term mixfix list *
-    (string * string) list)) list -> theory -> theory
-  val assoc_types: (xstring * (typ mixfix list *
-    (string * string) list)) list -> theory -> theory
-  val get_assoc_code: theory -> string -> typ ->
+  val assoc_const: string * (term mixfix list *
+    (string * string) list) -> theory -> theory
+  val assoc_const_i: (string * typ) * (term mixfix list *
+    (string * string) list) -> theory -> theory
+  val assoc_type: xstring * (typ mixfix list *
+    (string * string) list) -> theory -> theory
+  val get_assoc_code: theory -> string * typ ->
     (term mixfix list * (string * string) list) option
   val get_assoc_type: theory -> string ->
     (typ mixfix list * (string * string) list) option
@@ -384,46 +384,34 @@
 
 (**** associate constants with target language code ****)
 
-fun gen_assoc_consts prep_type xs thy = Library.foldl (fn (thy, (s, tyopt, syn)) =>
+fun gen_assoc_const prep_const (raw_const, syn) thy =
   let
     val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
       CodegenData.get thy;
-    val cname = Sign.intern_const thy s;
+    val (cname, T) = prep_const thy raw_const;
   in
-    (case Sign.const_type thy cname of
-       SOME T =>
-         let val T' = (case tyopt of
-                NONE => T
-              | SOME ty =>
-                  let val U = prep_type thy ty
-                  in if Type.raw_instance (U, T) then U
-                    else error ("Illegal type constraint for constant " ^ cname)
-                  end)
-         in
-           if num_args_of (fst syn) > length (binder_types T') then
-             error ("More arguments than in corresponding type of " ^ s)
-           else (case AList.lookup (op =) consts (cname, T') of
-             NONE => CodegenData.put {codegens = codegens,
-               tycodegens = tycodegens,
-               consts = ((cname, T'), syn) :: consts,
-               types = types, attrs = attrs, preprocs = preprocs,
-               modules = modules, test_params = test_params} thy
-           | SOME _ => error ("Constant " ^ cname ^ " already associated with code"))
-         end
-     | _ => error ("Not a constant: " ^ s))
-  end) (thy, xs);
+    if num_args_of (fst syn) > length (binder_types T) then
+      error ("More arguments than in corresponding type of " ^ cname)
+    else case AList.lookup (op =) consts (cname, T) of
+      NONE => CodegenData.put {codegens = codegens,
+        tycodegens = tycodegens,
+        consts = ((cname, T), syn) :: consts,
+        types = types, attrs = attrs, preprocs = preprocs,
+        modules = modules, test_params = test_params} thy
+    | SOME _ => error ("Constant " ^ cname ^ " already associated with code")
+  end;
 
-val assoc_consts_i = gen_assoc_consts (K I);
-val assoc_consts = gen_assoc_consts Sign.read_typ;
+val assoc_const_i = gen_assoc_const (K I);
+val assoc_const = gen_assoc_const CodegenConsts.read_bare_const;
 
 
 (**** associate types with target language types ****)
 
-fun assoc_types xs thy = Library.foldl (fn (thy, (s, syn)) =>
+fun assoc_type (s, syn) thy =
   let
     val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
       CodegenData.get thy;
-    val tc = Sign.intern_type thy s
+    val tc = Sign.intern_type thy s;
   in
     case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
       SOME (Type.LogicalType i, _) =>
@@ -436,7 +424,7 @@
             preprocs = preprocs, modules = modules, test_params = test_params} thy
         | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
     | _ => error ("Not a type constructor: " ^ s)
-  end) (thy, xs);
+  end;
 
 fun get_assoc_type thy = AList.lookup (op =) ((#types o CodegenData.get) thy);
 
@@ -581,7 +569,7 @@
 fun is_instance thy T1 T2 =
   Sign.typ_instance thy (T1, Logic.legacy_varifyT T2);
 
-fun get_assoc_code thy s T = Option.map snd (find_first (fn ((s', T'), _) =>
+fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
   s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
 
 fun get_aux_code xs = map_filter (fn (m, code) =>
@@ -734,7 +722,7 @@
         in SOME (gr'', mk_app brack (Pretty.str s) ps) end
 
     | Const (s, T) =>
-      (case get_assoc_code thy s T of
+      (case get_assoc_code thy (s, T) of
          SOME (ms, aux) =>
            let val i = num_args_of ms
            in if length ts < i then
@@ -1111,7 +1099,7 @@
    | _ => error ("Malformed annotation: " ^ quote s));
 
 val _ = Context.add_setup
-  (assoc_types [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
+  (fold assoc_type [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
      [("term_of",
        "fun term_of_fun_type _ T _ U _ = Free (\"<function>\", T --> U);\n"),
       ("test",
@@ -1139,19 +1127,19 @@
   OuterSyntax.command "types_code"
   "associate types with target language types" K.thy_decl
     (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
-     (fn xs => Toplevel.theory (fn thy => assoc_types
-       (map (fn ((name, mfx), aux) => (name, (parse_mixfix
-         (Sign.read_typ thy) mfx, aux))) xs) thy)));
+     (fn xs => Toplevel.theory (fn thy => fold (assoc_type o
+       (fn ((name, mfx), aux) => (name, (parse_mixfix
+         (Sign.read_typ thy) mfx, aux)))) xs thy)));
 
 val assoc_constP =
   OuterSyntax.command "consts_code"
   "associate constants with target language code" K.thy_decl
     (Scan.repeat1
-       (P.xname -- (Scan.option (P.$$$ "::" |-- P.typ)) --|
+       (P.term --|
         P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
-     (fn xs => Toplevel.theory (fn thy => assoc_consts
-       (map (fn (((name, optype), mfx), aux) =>
-         (name, optype, (parse_mixfix (Sign.read_term thy) mfx, aux))) xs) thy)));
+     (fn xs => Toplevel.theory (fn thy => fold (assoc_const o 
+       (fn ((const, mfx), aux) =>
+         (const, (parse_mixfix (Sign.read_term thy) mfx, aux)))) xs thy)));
 
 fun parse_code lib =
   Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) --