# HG changeset patch
# User wenzelm
# Date 1258061394 -3600
# Node ID 5266a72e08895e186e00161f171db3e1425a888a
# Parent  b275f26a638b0cecec75e1e439527778179a1ff0
eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";

diff -r b275f26a638b -r 5266a72e0889 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Nov 12 22:02:11 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Thu Nov 12 22:29:54 2009 +0100
@@ -713,7 +713,7 @@
       fold_map (fn (a, spec) => fn axs =>
           let val (ps, qs) = chop (length spec) axs
           in ((a, [(ps, [])]), qs) end) asms axms
-      |> apfst (curry Notes Thm.assumptionK)
+      |> apfst (curry Notes "")
   | assumes_to_notes e axms = (e, axms);
 
 fun defines_to_notes thy (Defines defs) =
diff -r b275f26a638b -r 5266a72e0889 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Nov 12 22:02:11 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Nov 12 22:29:54 2009 +0100
@@ -1126,7 +1126,7 @@
   in
     ctxt2
     |> auto_bind_facts (flat propss)
-    |> note_thmss Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
+    |> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss)
   end;
 
 in
diff -r b275f26a638b -r 5266a72e0889 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Nov 12 22:02:11 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Nov 12 22:29:54 2009 +0100
@@ -172,7 +172,7 @@
         #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])])));
 
     (*facts*)
-    val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
+    val (facts, thy') = axioms_thy |> PureThy.note_thmss ""
       (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
 
     val _ =
@@ -329,8 +329,9 @@
         val (facts, goal_ctxt) = elems_ctxt
           |> (snd o ProofContext.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
           |> fold_map assume_case (obtains ~~ propp)
-          |-> (fn ths => ProofContext.note_thmss Thm.assumptionK
-                [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
+          |-> (fn ths =>
+            ProofContext.note_thmss "" [((Binding.name Obtain.thatN, []), [(ths, [])])] #>
+            #2 #> pair ths);
       in ((prems, stmt, SOME facts), goal_ctxt) end);
 
 structure TheoremHook = Generic_Data
@@ -372,8 +373,7 @@
       end;
   in
     goal_ctxt
-    |> ProofContext.note_thmss Thm.assumptionK
-      [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
+    |> ProofContext.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
     |> snd
     |> Proof.theorem_i before_qed after_qed' (map snd stmt)
     |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
diff -r b275f26a638b -r 5266a72e0889 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Nov 12 22:02:11 2009 +0100
+++ b/src/Pure/more_thm.ML	Thu Nov 12 22:29:54 2009 +0100
@@ -84,8 +84,6 @@
   val has_name_hint: thm -> bool
   val get_name_hint: thm -> string
   val put_name_hint: string -> thm -> thm
-  val axiomK: string
-  val assumptionK: string
   val definitionK: string
   val theoremK: string
   val generatedK : string
@@ -413,8 +411,6 @@
 
 (* theorem kinds *)
 
-val axiomK = "axiom";
-val assumptionK = "assumption";
 val definitionK = "definition";
 val theoremK = "theorem";
 val generatedK = "generatedK"