--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Thu Apr 18 17:07:01 2013 +0200
@@ -192,8 +192,8 @@
EVERY [
rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
ALLGOALS (EVERY'
- [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
- resolve_tac prems, asm_simp_tac HOL_basic_ss])])
+ [asm_simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps case_rewrites),
+ resolve_tac prems, asm_simp_tac (Simplifier.global_context thy HOL_basic_ss)])])
|> Drule.export_without_context;
val exh_name = Thm.derivation_name exhaust;