--- 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
*}