# HG changeset patch
# User haftmann
# Date 1242537459 -7200
# Node ID 92e0ed53db251e2fb27d8e1dcd4525e73e572d66
# Parent  9b1e7159f4e51b857ff86983570c9be604715226
is a definition

diff -r 9b1e7159f4e5 -r 92e0ed53db25 src/HOL/String.thy
--- a/src/HOL/String.thy	Sat May 16 20:18:26 2009 +0200
+++ b/src/HOL/String.thy	Sun May 17 07:17:39 2009 +0200
@@ -55,7 +55,7 @@
    (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
       nibbles nibbles;
 in
-  PureThy.note_thmss Thm.generated_theoremK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
+  PureThy.note_thmss Thm.definitionK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
   #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
 end
 *}