--- a/src/Pure/Isar/specification.ML Tue Jan 10 19:33:38 2006 +0100
+++ b/src/Pure/Isar/specification.ML Tue Jan 10 19:33:39 2006 +0100
@@ -8,23 +8,24 @@
signature SPECIFICATION =
sig
- val pretty_consts: theory -> (string * typ) list -> Pretty.T
+ val pretty_consts: Proof.context -> (string * typ) list -> Pretty.T
val read_specification:
- (string * string option * mixfix) list * ((string * Attrib.src list) * string list) list ->
- Proof.context ->
- ((string * typ * mixfix) list * ((string * theory attribute list) * term list) list) *
- Proof.context
+ (string * string option * mixfix) list *
+ ((string * Attrib.src list) * string list) list -> Proof.context ->
+ ((string * typ * mixfix) list *
+ ((string * Context.generic attribute list) * term list) list) * Proof.context
val cert_specification:
- (string * typ option * mixfix) list * ((string * theory attribute list) * term list) list ->
- Proof.context ->
- ((string * typ * mixfix) list * ((string * theory attribute list) * term list) list) *
- Proof.context
+ (string * typ option * mixfix) list *
+ ((string * Context.generic attribute list) * term list) list -> Proof.context ->
+ ((string * typ * mixfix) list *
+ ((string * Context.generic attribute list) * term list) list) * Proof.context
val axiomatize:
- (string * string option * mixfix) list * ((bstring * Attrib.src list) * string list) list ->
- theory -> thm list list * theory
+ (string * string option * mixfix) list *
+ ((bstring * Attrib.src list) * string list) list -> theory -> thm list list * theory
val axiomatize_i:
- (string * typ option * mixfix) list * ((bstring * theory attribute list) * term list) list ->
- theory -> thm list list * theory
+ (string * typ option * mixfix) list *
+ ((bstring * Context.generic attribute list) * term list) list -> theory ->
+ thm list list * theory
end;
structure Specification: SPECIFICATION =
@@ -32,12 +33,12 @@
(* pretty_consts *)
-fun pretty_const thy (c, T) =
+fun pretty_const ctxt (c, T) =
Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
- Pretty.quote (Sign.pretty_typ thy T)];
+ Pretty.quote (ProofContext.pretty_typ ctxt T)];
-fun pretty_consts thy decls =
- Pretty.big_list "constants" (map (pretty_const thy) decls);
+fun pretty_consts ctxt decls =
+ Pretty.big_list "constants" (map (pretty_const ctxt) decls);
(* prepare specification *)
@@ -64,7 +65,7 @@
in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end;
fun read_specification x =
- prep_specification ProofContext.read_typ ProofContext.read_propp Attrib.global_attribute x;
+ prep_specification ProofContext.read_typ ProofContext.read_propp Attrib.generic_attribute x;
fun cert_specification x =
prep_specification ProofContext.cert_typ ProofContext.cert_propp (K I) x;
@@ -74,15 +75,15 @@
fun gen_axiomatize prep args thy =
let
val ((consts, specs), ctxt) = prep args (ProofContext.init thy);
- val subst = map (fn (x, T, _) => (Free (x, T), Const (Sign.full_name thy x, T))) consts;
- val axioms =
- map (fn ((name, att), ts) => ((name, map (Term.subst_atomic subst) ts), att)) specs;
+ val subst = consts |> map (fn (x, T, _) => (Free (x, T), Const (Sign.full_name thy x, T)));
+ val axioms = specs |> map (fn ((name, att), ts) =>
+ ((name, map (Term.subst_atomic subst) ts), map Attrib.theory att));
val (thms, thy') =
thy
|> Theory.add_consts_i consts
|> PureThy.add_axiomss_i axioms
||> Theory.add_finals_i false (map snd subst);
- in Pretty.writeln (pretty_consts thy' (map (dest_Free o fst) subst)); (thms, thy') end;
+ in Pretty.writeln (pretty_consts ctxt (map (dest_Free o fst) subst)); (thms, thy') end;
val axiomatize = gen_axiomatize read_specification;
val axiomatize_i = gen_axiomatize cert_specification;