# HG changeset patch
# User wenzelm
# Date 1138059814 -3600
# Node ID 63efe00371afe45f0de32f6c79961de7e3ec0feb
# Parent  434f660d30684814dc92403f1517234ebe9e2992
renamed axiomatize(_i) to axiomatization(_i);
LocalTheory;

diff -r 434f660d3068 -r 63efe00371af src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Jan 24 00:43:33 2006 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Jan 24 00:43:34 2006 +0100
@@ -2,49 +2,35 @@
     ID:         $Id$
     Author:     Makarius
 
-Theory specifications --- with type-inference, but no internal
-polymorphism.
+Common theory/locale specifications --- with type-inference, but
+without internal polymorphism.
 *)
 
 signature SPECIFICATION =
 sig
-  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 * attribute list) * term list) list) * Proof.context
-  val cert_specification:
-    (string * typ option * mixfix) list *
-      ((string * attribute list) * term list) list -> Proof.context ->
-    ((string * typ * mixfix) list *
-      ((string * 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
-  val axiomatize_i:
-    (string * typ option * mixfix) list *
-      ((bstring * attribute list) * term list) list -> theory ->
-    thm list list * theory
+  val read_specification: (string * string option * mixfix) list ->
+    ((string * Attrib.src list) * string list) list -> Proof.context ->
+    (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
+    Proof.context
+  val cert_specification: (string * typ option * mixfix) list ->
+    ((string * Attrib.src list) * term list) list -> Proof.context ->
+    (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
+    Proof.context
+  val axiomatization: xstring option -> (string * string option * mixfix) list ->
+    ((bstring * Attrib.src list) * string list) list -> theory ->
+    (term list * (bstring * thm list) list) * (theory * Proof.context)
+  val axiomatization_i: string option -> (string * typ option * mixfix) list ->
+    ((bstring * Attrib.src list) * term list) list -> theory ->
+    (term list * (bstring * thm list) list) * (theory * Proof.context)
 end;
 
 structure Specification: SPECIFICATION =
 struct
 
-(* pretty_consts *)
-
-fun pretty_const ctxt (c, T) =
-  Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
-    Pretty.quote (ProofContext.pretty_typ ctxt T)];
-
-fun pretty_consts ctxt decls =
-  Pretty.big_list "constants" (map (pretty_const ctxt) decls);
-
-
 (* prepare specification *)
 
 fun prep_specification prep_vars prep_propp prep_att
-    (raw_vars, raw_specs) ctxt =
+    raw_vars raw_specs ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
 
@@ -53,35 +39,34 @@
     val ((specs, vs), specs_ctxt) =
       prep_propp (params_ctxt, map (map (rpair ([], [])) o snd) raw_specs)
       |> swap |>> map (map fst)
-      ||>> fold_map ProofContext.inferred_type xs;
+      ||>> fold_map ProofContext.inferred_param xs;
 
-    val params = map2 (fn (x, T) => fn (_, _, mx) => (x, T, mx)) vs vars;
+    val params = vs ~~ map #3 vars;
     val names = map (fst o fst) raw_specs;
     val atts = map (map (prep_att thy) o snd o fst) raw_specs;
   in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end;
 
 fun read_specification x =
-  prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.attribute x;
+  prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.intern_src x;
 fun cert_specification x =
   prep_specification ProofContext.cert_vars ProofContext.cert_propp (K I) x;
 
 
-(* axiomatize *)
+(* axiomatization *)
 
-fun gen_axiomatize prep args thy =
+fun gen_axiomatization prep init locale raw_vars raw_specs thy =
   let
-    val ((consts, specs), ctxt) = prep args (ProofContext.init thy);
-    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), 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 ctxt (map (dest_Free o fst) subst)); (thms, thy') end;
+    val ((vars, specs), ctxt) = init locale thy |> prep raw_vars raw_specs;
+    val (consts, consts_ctxt) = ctxt |> LocalTheory.consts vars;
+    val subst = Term.subst_atomic (map (Free o fst) vars ~~ consts);
+    val (axioms, axioms_ctxt) =
+      consts_ctxt
+      |> LocalTheory.axioms (specs |> map (fn (a, props) => (a, map subst props)))
+      ||> LocalTheory.map_theory (Theory.add_finals_i false (map Term.head_of consts));
+    val _ = Pretty.writeln (LocalTheory.pretty_consts ctxt (map fst vars));
+  in ((consts, axioms), `LocalTheory.exit axioms_ctxt) end;
 
-val axiomatize = gen_axiomatize read_specification;
-val axiomatize_i = gen_axiomatize cert_specification;
+val axiomatization = gen_axiomatization read_specification LocalTheory.init;
+val axiomatization_i = gen_axiomatization cert_specification LocalTheory.init_i;
 
 end;