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