src/HOL/Product_Type.thy
changeset 62913 13252110a6fe
parent 62594 75452e3eda14
child 63007 aa894a49f77d
     1.1 --- a/src/HOL/Product_Type.thy	Thu Apr 07 22:09:23 2016 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Apr 08 20:15:20 2016 +0200
     1.3 @@ -1327,8 +1327,7 @@
     1.4    Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs
     1.5      [Simplifier.make_simproc @{context} "set comprehension"
     1.6        {lhss = [@{term "Collect P"}],
     1.7 -       proc = K Set_Comprehension_Pointfree.code_simproc,
     1.8 -       identifier = []}])
     1.9 +       proc = K Set_Comprehension_Pointfree.code_simproc}])
    1.10  \<close>
    1.11  
    1.12