src/HOL/String.thy
changeset 38808 89ae86205739
parent 37743 0a3fa8fbcdc5
child 38858 1920158cfa17
--- a/src/HOL/String.thy	Fri Aug 27 17:23:57 2010 +0200
+++ b/src/HOL/String.thy	Fri Aug 27 17:59:40 2010 +0200
@@ -53,7 +53,7 @@
    (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
       nibbles nibbles;
 in
-  PureThy.note_thmss Thm.definitionK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
+  PureThy.note_thmss Thm.definitionK [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
   #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
 end
 *}