src/HOL/String.thy
changeset 39557 fe5722fce758
parent 39302 d7728f65b353
child 41750 2b4f7a29126f
     1.1 --- a/src/HOL/String.thy	Mon Sep 20 15:29:53 2010 +0200
     1.2 +++ b/src/HOL/String.thy	Mon Sep 20 16:05:25 2010 +0200
     1.3 @@ -53,7 +53,8 @@
     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.definitionK [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
     1.8 +  Global_Theory.note_thmss Thm.definitionK
     1.9 +    [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
    1.10    #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
    1.11  end
    1.12  *}