# HG changeset patch
# User wenzelm
# Date 1220456860 -7200
# Node ID cd0d170d4dc6084d0e6f0a40b3911c8aae52cb4b
# Parent  2637fb838f743857c362cc66e9687ca1cfa3231a
discontinued local axioms -- too difficult to implement, too easy to produce nonsense;

diff -r 2637fb838f74 -r cd0d170d4dc6 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed Sep 03 17:47:38 2008 +0200
+++ b/src/Pure/Isar/local_theory.ML	Wed Sep 03 17:47:40 2008 +0200
@@ -25,9 +25,6 @@
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val affirm: local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
-  val axioms: string ->
-    ((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list -> local_theory
-    -> (term list * (string * thm list) list) * local_theory
   val abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
   val define: string -> (Name.binding * mixfix) * (Attrib.binding * term) -> local_theory ->
@@ -55,9 +52,6 @@
 
 type operations =
  {pretty: local_theory -> Pretty.T list,
-  axioms: string ->
-    ((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list -> local_theory ->
-    (term list * (string * thm list) list) * local_theory,
   abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
   define: string ->
@@ -171,7 +165,6 @@
 fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy;
 
 val pretty = operation #pretty;
-val axioms = operation2 #axioms;
 val abbrev = operation2 #abbrev;
 val define = operation2 #define;
 val notes = operation2 #notes;
diff -r 2637fb838f74 -r cd0d170d4dc6 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Sep 03 17:47:38 2008 +0200
+++ b/src/Pure/Isar/theory_target.ML	Wed Sep 03 17:47:40 2008 +0200
@@ -226,7 +226,7 @@
                 if mx3 <> NoSyn then syntax_error c'
                 else LocalTheory.theory_result (Overloading.declare (c', U))
                   ##> Overloading.confirm c
-            | NONE => LocalTheory.theory_result (Sign.declare_const tags (c, U, mx3))));
+            | NONE => LocalTheory.theory_result (Sign.declare_const tags ((b, U), mx3))));
     val (const, lthy') = lthy |> declare_const;
     val t = Term.list_comb (const, map Free xs);
   in
@@ -311,33 +311,6 @@
   in ((lhs, (res_name, res)), lthy4) end;
 
 
-(* axioms *)
-
-fun axioms ta kind (vars, specs) lthy =
-  let
-    val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
-    val expanded_props = map (Assumption.export_term lthy thy_ctxt) (maps snd specs);
-    val xs = fold Term.add_frees expanded_props [];
-
-    (*consts*)
-    val (consts, lthy') = fold_map (declare_const ta (member (op =) xs)) vars lthy;
-    val global_consts = map (Term.dest_Const o Term.head_of o Thm.term_of o Thm.rhs_of o #2) consts;
-
-    (*axioms*)
-    val hyps = map Thm.term_of (Assumption.assms_of lthy');
-    fun axiom ((name, atts), props) thy = thy
-      |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi (Name.name_of name) props)
-      |-> (fn ths => pair ((name, atts), [(ths, [])]));
-  in
-    lthy'
-    |> fold Variable.declare_term expanded_props
-    |> LocalTheory.theory (fold (fn c => Theory.add_deps "" c []) global_consts)
-    |> LocalTheory.theory_result (fold_map axiom specs)
-    |-> notes ta kind
-    |>> pair (map #1 consts)
-  end;
-
-
 (* init *)
 
 local
@@ -357,7 +330,6 @@
   Data.put ta #>
   LocalTheory.init (NameSpace.base target)
    {pretty = pretty ta,
-    axioms = axioms ta,
     abbrev = abbrev ta,
     define = define ta,
     notes = notes ta,