src/Pure/Isar/specification.ML
changeset 28114 2637fb838f74
parent 28093 d81a4ed6b538
child 28370 37f56e6e702d
     1.1 --- a/src/Pure/Isar/specification.ML	Wed Sep 03 17:47:37 2008 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Wed Sep 03 17:47:38 2008 +0200
     1.3 @@ -22,11 +22,11 @@
     1.4      (Attrib.binding * string list) list -> Proof.context ->
     1.5      (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
     1.6    val axiomatization: (Name.binding * typ option * mixfix) list ->
     1.7 -    (Attrib.binding * term list) list -> local_theory ->
     1.8 -    (term list * (string * thm list) list) * local_theory
     1.9 +    (Attrib.binding * term list) list -> theory ->
    1.10 +    (term list * (string * thm list) list) * theory
    1.11    val axiomatization_cmd: (Name.binding * string option * mixfix) list ->
    1.12 -    (Attrib.binding * string list) list -> local_theory ->
    1.13 -    (term list * (string * thm list) list) * local_theory
    1.14 +    (Attrib.binding * string list) list -> theory ->
    1.15 +    (term list * (string * thm list) list) * theory
    1.16    val definition:
    1.17      (Name.binding * typ option * mixfix) option * (Attrib.binding * term) ->
    1.18      local_theory -> (term * (string * thm)) * local_theory
    1.19 @@ -137,18 +137,27 @@
    1.20  end;
    1.21  
    1.22  
    1.23 -(* axiomatization *)
    1.24 +(* axiomatization -- within global theory *)
    1.25  
    1.26 -fun gen_axioms do_print prep raw_vars raw_specs lthy =
    1.27 +fun gen_axioms do_print prep raw_vars raw_specs thy =
    1.28    let
    1.29 -    val ((vars, specs), _) = prep raw_vars [raw_specs] lthy;
    1.30 -    val ((consts, axioms), lthy') = LocalTheory.axioms Thm.axiomK (vars, specs) lthy;
    1.31 -    val consts' = map (Morphism.term (LocalTheory.target_morphism lthy')) consts;
    1.32 +    val ((vars, specs), _) = prep raw_vars [raw_specs] (ProofContext.init thy);
    1.33 +    val xs = map (fn ((b, T), _) => (Name.name_of b, T)) vars;
    1.34 +
    1.35 +    (*consts*)
    1.36 +    val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
    1.37 +    val subst = Term.subst_atomic (map Free xs ~~ consts);
    1.38 +
    1.39 +    (*axioms*)
    1.40 +    val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
    1.41 +        fold_map Thm.add_axiom (PureThy.name_multi (Name.name_of b) (map subst props))
    1.42 +        #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
    1.43 +    val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
    1.44 +      (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
    1.45      val _ =
    1.46        if not do_print then ()
    1.47 -      else print_consts lthy' (member (op =) (fold Term.add_frees consts' []))
    1.48 -        (map (fn ((b, T), _) => (Name.name_of b, T)) vars);
    1.49 -  in ((consts, axioms), lthy') end;
    1.50 +      else print_consts (ProofContext.init thy') (K false) xs;
    1.51 +  in ((consts, facts), thy') end;
    1.52  
    1.53  val axiomatization = gen_axioms false check_specification;
    1.54  val axiomatization_cmd = gen_axioms true read_specification;