discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
authorwenzelm
Wed Sep 03 17:47:40 2008 +0200 (2008-09-03)
changeset 28115cd0d170d4dc6
parent 28114 2637fb838f74
child 28116 cd2547ab0696
discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
src/Pure/Isar/local_theory.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Wed Sep 03 17:47:38 2008 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Sep 03 17:47:40 2008 +0200
     1.3 @@ -25,9 +25,6 @@
     1.4    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
     1.5    val affirm: local_theory -> local_theory
     1.6    val pretty: local_theory -> Pretty.T list
     1.7 -  val axioms: string ->
     1.8 -    ((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list -> local_theory
     1.9 -    -> (term list * (string * thm list) list) * local_theory
    1.10    val abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
    1.11      (term * term) * local_theory
    1.12    val define: string -> (Name.binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    1.13 @@ -55,9 +52,6 @@
    1.14  
    1.15  type operations =
    1.16   {pretty: local_theory -> Pretty.T list,
    1.17 -  axioms: string ->
    1.18 -    ((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list -> local_theory ->
    1.19 -    (term list * (string * thm list) list) * local_theory,
    1.20    abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
    1.21      (term * term) * local_theory,
    1.22    define: string ->
    1.23 @@ -171,7 +165,6 @@
    1.24  fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy;
    1.25  
    1.26  val pretty = operation #pretty;
    1.27 -val axioms = operation2 #axioms;
    1.28  val abbrev = operation2 #abbrev;
    1.29  val define = operation2 #define;
    1.30  val notes = operation2 #notes;
     2.1 --- a/src/Pure/Isar/theory_target.ML	Wed Sep 03 17:47:38 2008 +0200
     2.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Sep 03 17:47:40 2008 +0200
     2.3 @@ -226,7 +226,7 @@
     2.4                  if mx3 <> NoSyn then syntax_error c'
     2.5                  else LocalTheory.theory_result (Overloading.declare (c', U))
     2.6                    ##> Overloading.confirm c
     2.7 -            | NONE => LocalTheory.theory_result (Sign.declare_const tags (c, U, mx3))));
     2.8 +            | NONE => LocalTheory.theory_result (Sign.declare_const tags ((b, U), mx3))));
     2.9      val (const, lthy') = lthy |> declare_const;
    2.10      val t = Term.list_comb (const, map Free xs);
    2.11    in
    2.12 @@ -311,33 +311,6 @@
    2.13    in ((lhs, (res_name, res)), lthy4) end;
    2.14  
    2.15  
    2.16 -(* axioms *)
    2.17 -
    2.18 -fun axioms ta kind (vars, specs) lthy =
    2.19 -  let
    2.20 -    val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    2.21 -    val expanded_props = map (Assumption.export_term lthy thy_ctxt) (maps snd specs);
    2.22 -    val xs = fold Term.add_frees expanded_props [];
    2.23 -
    2.24 -    (*consts*)
    2.25 -    val (consts, lthy') = fold_map (declare_const ta (member (op =) xs)) vars lthy;
    2.26 -    val global_consts = map (Term.dest_Const o Term.head_of o Thm.term_of o Thm.rhs_of o #2) consts;
    2.27 -
    2.28 -    (*axioms*)
    2.29 -    val hyps = map Thm.term_of (Assumption.assms_of lthy');
    2.30 -    fun axiom ((name, atts), props) thy = thy
    2.31 -      |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi (Name.name_of name) props)
    2.32 -      |-> (fn ths => pair ((name, atts), [(ths, [])]));
    2.33 -  in
    2.34 -    lthy'
    2.35 -    |> fold Variable.declare_term expanded_props
    2.36 -    |> LocalTheory.theory (fold (fn c => Theory.add_deps "" c []) global_consts)
    2.37 -    |> LocalTheory.theory_result (fold_map axiom specs)
    2.38 -    |-> notes ta kind
    2.39 -    |>> pair (map #1 consts)
    2.40 -  end;
    2.41 -
    2.42 -
    2.43  (* init *)
    2.44  
    2.45  local
    2.46 @@ -357,7 +330,6 @@
    2.47    Data.put ta #>
    2.48    LocalTheory.init (NameSpace.base target)
    2.49     {pretty = pretty ta,
    2.50 -    axioms = axioms ta,
    2.51      abbrev = abbrev ta,
    2.52      define = define ta,
    2.53      notes = notes ta,