# HG changeset patch
# User berghofe
# Date 1196258198 -3600
# Node ID d96d5808d92673dee45d654c59730eacf14238ef
# Parent  b944ef973109a08f89eff30a760fc58fbb1137d8
to_set now applies collect_mem_simproc as well.

diff -r b944ef973109 -r d96d5808d926 src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Wed Nov 28 09:01:50 2007 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Wed Nov 28 14:56:38 2007 +0100
@@ -371,7 +371,7 @@
     thm |>
     Thm.instantiate ([], insts) |>
     Simplifier.full_simplify (HOL_basic_ss addsimps to_set_simps
-        addsimprocs [strong_ind_simproc pred_arities]) |>
+        addsimprocs [strong_ind_simproc pred_arities, collect_mem_simproc]) |>
     RuleCases.save thm
   end;