src/HOL/String.thy
changeset 31174 f1f1e9b53c81
parent 31055 2cf6efca6c71
child 31176 92e0ed53db25
     1.1 --- a/src/HOL/String.thy	Sat May 16 15:24:35 2009 +0200
     1.2 +++ b/src/HOL/String.thy	Sat May 16 20:17:59 2009 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4     (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
     1.5        nibbles nibbles;
     1.6  in
     1.7 -  PureThy.note_thmss Thm.lemmaK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
     1.8 +  PureThy.note_thmss Thm.generated_theoremK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
     1.9    #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
    1.10  end
    1.11  *}