--- a/src/HOL/Tools/choice_specification.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/choice_specification.ML Fri Mar 06 23:56:43 2015 +0100
@@ -83,7 +83,7 @@
val ctxt = Proof_Context.init_global thy
val rew_imps = alt_props |>
- map (Object_Logic.atomize ctxt o Thm.global_cterm_of thy o Syntax.read_prop_global thy o snd)
+ map (Object_Logic.atomize ctxt o Thm.cterm_of ctxt o Syntax.read_prop_global thy o snd)
val props' = rew_imps |>
map (HOLogic.dest_Trueprop o Thm.term_of o snd o Thm.dest_equals o Thm.cprop_of)