--- a/src/HOL/Tools/choice_specification.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML Mon Sep 20 16:05:25 2010 +0200
@@ -33,7 +33,7 @@
else thname
val def_eq = Logic.mk_equals (Const(cname_full,ctype),
HOLogic.choice_const ctype $ P)
- val (thms, thy') = PureThy.add_defs covld [((Binding.name cdefname, def_eq),[])] thy
+ val (thms, thy') = Global_Theory.add_defs covld [((Binding.name cdefname, def_eq),[])] thy
val thm' = [thm,hd thms] MRS @{thm exE_some}
in
mk_definitional cos (thy',thm')
@@ -189,7 +189,7 @@
if name = ""
then arg |> Library.swap
else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
- PureThy.store_thm (Binding.name name, thm) thy)
+ Global_Theory.store_thm (Binding.name name, thm) thy)
in
args |> apsnd (remove_alls frees)
|> apsnd undo_imps