src/HOL/Tools/Function/sum_tree.ML

--- a/src/HOL/Tools/Function/sum_tree.ML	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Tools/Function/sum_tree.ML	Thu Apr 18 17:07:01 2013 +0200
@@ -21,7 +21,8 @@
 
 (* Theory dependencies *)
 val sumcase_split_ss =
-  HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases})
+  simpset_of (put_simpset HOL_basic_ss @{context}
+    addsimps (@{thm Product_Type.split} :: @{thms sum.cases}))
 
 (* top-down access in balanced tree *)
 fun access_top_down {left, right, init} len i =