# HG changeset patch # User wenzelm # Date 1147808001 -7200 # Node ID e1dc01a48a523994539ca03ee927f610449dd2fc # Parent 459848022d6e498912d3dee8f4afdf8487366b67 added const_syntax(_i); diff -r 459848022d6e -r e1dc01a48a52 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Tue May 16 21:33:18 2006 +0200 +++ b/src/Pure/Isar/specification.ML Tue May 16 21:33:21 2006 +0200 @@ -2,7 +2,7 @@ ID: $Id$ Author: Makarius -Common theory/locale specifications --- with type-inference and +Common local_theory specifications --- with type-inference and toplevel polymorphism. *) @@ -32,11 +32,14 @@ local_theory -> local_theory val abbreviation_i: string * bool -> ((string * typ option * mixfix) option * term) list -> local_theory -> local_theory + val const_syntax: string * bool -> (xstring * mixfix) list -> local_theory -> local_theory + val const_syntax_i: string * bool -> (string * mixfix) list -> local_theory -> local_theory end; structure Specification: SPECIFICATION = struct + (* prepare specification *) fun prep_specification prep_vars prep_propp prep_att raw_vars raw_specs ctxt = @@ -124,18 +127,28 @@ else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote x')); in ctxt' - |> LocalTheory.abbrev mode ((x, mx), rhs) + |> LocalTheory.abbrevs mode [((x, mx), rhs)] |> pair (x, T) end; - val (cs, abbrs_ctxt) = ctxt + val (cs, result_ctxt) = ctxt |> ProofContext.set_syntax_mode mode |> fold_map abbrev args ||> ProofContext.restore_syntax_mode ctxt; val _ = LocalTheory.print_consts ctxt (K false) cs; - in abbrs_ctxt end; + in result_ctxt end; val abbreviation = gen_abbrevs read_specification; val abbreviation_i = gen_abbrevs cert_specification; + +(* const syntax *) + +fun gen_syntax intern_const mode raw_args ctxt = + let val args = raw_args |> map (apfst (intern_const (ProofContext.consts_of ctxt))) + in ctxt |> LocalTheory.syntax mode args end; + +val const_syntax = gen_syntax Consts.intern; +val const_syntax_i = gen_syntax (K I); + end;