--- 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 #)
--- 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
--- 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;
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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 {*
--- 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
--- 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
--- 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\"")
--- 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\"")
--- 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);
--- 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
--- 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) =>
--- 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 =
--- 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) --