src/Pure/Isar/class.ML
changeset 39557 fe5722fce758
parent 39438 c5ece2a7a86e
child 40627 becf5d5187cc
     1.1 --- a/src/Pure/Isar/class.ML	Mon Sep 20 15:29:53 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Sep 20 16:05:25 2010 +0200
     1.3 @@ -329,7 +329,7 @@
     1.4      |> snd
     1.5      |> Thm.add_def false false (b_def, def_eq)
     1.6      |>> apsnd Thm.varifyT_global
     1.7 -    |-> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm)
     1.8 +    |-> (fn (_, def_thm) => Global_Theory.store_thm (b_def, def_thm)
     1.9        #> snd
    1.10        #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
    1.11      |> Sign.add_const_constraint (c', SOME ty')