# HG changeset patch
# User wenzelm
# Date 1303383387 -7200
# Node ID 5e7a7343ab11be6133ab803cee57ee0250edc2c6
# Parent  9efdd0af15ac022eb0400d83e6563321dbbbce6e
discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;

diff -r 9efdd0af15ac -r 5e7a7343ab11 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Apr 20 22:57:29 2011 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Apr 21 12:56:27 2011 +0200
@@ -1018,8 +1018,7 @@
          ((mk_rulename id, []),
           [(term_of_rule thy' prfx types pfuns ids rl, [])]))
            other_rules),
-       Element.Notes (Thm.definitionK,
-         [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]
+       Element.Notes ("", [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]
           
   in
     set_env {ctxt = ctxt, defs = defs', types = types, funs = funs,
diff -r 9efdd0af15ac -r 5e7a7343ab11 src/HOL/String.thy
--- a/src/HOL/String.thy	Wed Apr 20 22:57:29 2011 +0200
+++ b/src/HOL/String.thy	Thu Apr 21 12:56:27 2011 +0200
@@ -53,7 +53,7 @@
    (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
       nibbles nibbles;
 in
-  Global_Theory.note_thmss Thm.definitionK
+  Global_Theory.note_thmss ""
     [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
   #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
 end
diff -r 9efdd0af15ac -r 5e7a7343ab11 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Apr 20 22:57:29 2011 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Apr 21 12:56:27 2011 +0200
@@ -725,7 +725,7 @@
   | assumes_to_notes e axms = (e, axms);
 
 fun defines_to_notes thy (Defines defs) =
-      Notes (Thm.definitionK, map (fn (a, (def, _)) =>
+      Notes ("", map (fn (a, (def, _)) =>
         (a, [([Assumption.assume (cterm_of thy def)],
           [(Attrib.internal o K) Locale.witness_add])])) defs)
   | defines_to_notes _ e = e;
diff -r 9efdd0af15ac -r 5e7a7343ab11 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Apr 20 22:57:29 2011 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Apr 21 12:56:27 2011 +0200
@@ -227,7 +227,7 @@
     val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
 
     val ([(def_name, [th'])], lthy4) = lthy3
-      |> Local_Theory.notes_kind Thm.definitionK
+      |> Local_Theory.notes_kind ""
         [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
 
     val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
diff -r 9efdd0af15ac -r 5e7a7343ab11 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Apr 20 22:57:29 2011 +0200
+++ b/src/Pure/more_thm.ML	Thu Apr 21 12:56:27 2011 +0200
@@ -87,7 +87,6 @@
   val has_name_hint: thm -> bool
   val get_name_hint: thm -> string
   val put_name_hint: string -> thm -> thm
-  val definitionK: string
   val theoremK: string
   val lemmaK: string
   val corollaryK: string
@@ -450,7 +449,6 @@
 
 (* theorem kinds *)
 
-val definitionK = "definition";
 val theoremK = "theorem";
 val lemmaK = "lemma";
 val corollaryK = "corollary";