--- a/src/HOL/Product_Type.thy Wed Sep 09 14:47:41 2015 +0200
+++ b/src/HOL/Product_Type.thy Wed Sep 09 20:57:21 2015 +0200
@@ -1261,8 +1261,10 @@
setup \<open>
Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs
- [Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}],
- proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}])
+ [Simplifier.make_simproc @{context} "set comprehension"
+ {lhss = [@{term "Collect P"}],
+ proc = K Set_Comprehension_Pointfree.code_simproc,
+ identifier = []}])
\<close>