discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
authorwenzelm
Thu Apr 21 12:56:27 2011 +0200 (2011-04-21)
changeset 424405e7a7343ab11
parent 42439 9efdd0af15ac
child 42441 781c622af16a
discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/String.thy
src/Pure/Isar/expression.ML
src/Pure/Isar/specification.ML
src/Pure/more_thm.ML
     1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Apr 20 22:57:29 2011 +0200
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Apr 21 12:56:27 2011 +0200
     1.3 @@ -1018,8 +1018,7 @@
     1.4           ((mk_rulename id, []),
     1.5            [(term_of_rule thy' prfx types pfuns ids rl, [])]))
     1.6             other_rules),
     1.7 -       Element.Notes (Thm.definitionK,
     1.8 -         [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]
     1.9 +       Element.Notes ("", [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]
    1.10            
    1.11    in
    1.12      set_env {ctxt = ctxt, defs = defs', types = types, funs = funs,
     2.1 --- a/src/HOL/String.thy	Wed Apr 20 22:57:29 2011 +0200
     2.2 +++ b/src/HOL/String.thy	Thu Apr 21 12:56:27 2011 +0200
     2.3 @@ -53,7 +53,7 @@
     2.4     (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
     2.5        nibbles nibbles;
     2.6  in
     2.7 -  Global_Theory.note_thmss Thm.definitionK
     2.8 +  Global_Theory.note_thmss ""
     2.9      [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
    2.10    #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
    2.11  end
     3.1 --- a/src/Pure/Isar/expression.ML	Wed Apr 20 22:57:29 2011 +0200
     3.2 +++ b/src/Pure/Isar/expression.ML	Thu Apr 21 12:56:27 2011 +0200
     3.3 @@ -725,7 +725,7 @@
     3.4    | assumes_to_notes e axms = (e, axms);
     3.5  
     3.6  fun defines_to_notes thy (Defines defs) =
     3.7 -      Notes (Thm.definitionK, map (fn (a, (def, _)) =>
     3.8 +      Notes ("", map (fn (a, (def, _)) =>
     3.9          (a, [([Assumption.assume (cterm_of thy def)],
    3.10            [(Attrib.internal o K) Locale.witness_add])])) defs)
    3.11    | defines_to_notes _ e = e;
     4.1 --- a/src/Pure/Isar/specification.ML	Wed Apr 20 22:57:29 2011 +0200
     4.2 +++ b/src/Pure/Isar/specification.ML	Thu Apr 21 12:56:27 2011 +0200
     4.3 @@ -227,7 +227,7 @@
     4.4      val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
     4.5  
     4.6      val ([(def_name, [th'])], lthy4) = lthy3
     4.7 -      |> Local_Theory.notes_kind Thm.definitionK
     4.8 +      |> Local_Theory.notes_kind ""
     4.9          [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
    4.10  
    4.11      val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
     5.1 --- a/src/Pure/more_thm.ML	Wed Apr 20 22:57:29 2011 +0200
     5.2 +++ b/src/Pure/more_thm.ML	Thu Apr 21 12:56:27 2011 +0200
     5.3 @@ -87,7 +87,6 @@
     5.4    val has_name_hint: thm -> bool
     5.5    val get_name_hint: thm -> string
     5.6    val put_name_hint: string -> thm -> thm
     5.7 -  val definitionK: string
     5.8    val theoremK: string
     5.9    val lemmaK: string
    5.10    val corollaryK: string
    5.11 @@ -450,7 +449,6 @@
    5.12  
    5.13  (* theorem kinds *)
    5.14  
    5.15 -val definitionK = "definition";
    5.16  val theoremK = "theorem";
    5.17  val lemmaK = "lemma";
    5.18  val corollaryK = "corollary";