changeset 39557 | fe5722fce758 |
parent 36960 | 01594f816e3a |
child 39965 | da88519e6a0b |
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Mon Sep 20 15:29:53 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Mon Sep 20 16:05:25 2010 +0200 @@ -194,7 +194,7 @@ ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info; in theorems_thy - |> PureThy.add_thmss + |> Global_Theory.add_thmss [((Binding.qualified true "rews" comp_dbind, flat rewss @ take_rews), [])] |> snd