# HG changeset patch
# User bulwahn
# Date 1349858863 -7200
# Node ID 9979d64b80169ea3e99c867bdadd4b099a1648cc
# Parent  bed063d0c5266d51e4d2b9028804811ada10998c
moving simproc from Finite_Set to more appropriate Product_Type theory

diff -r bed063d0c526 -r 9979d64b8016 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Oct 10 10:47:21 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Oct 10 10:47:43 2012 +0200
@@ -16,18 +16,7 @@
     emptyI [simp, intro!]: "finite {}"
   | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
 
-(* FIXME: move to Set theory *)
-ML_file "Tools/set_comprehension_pointfree.ML"
-
-simproc_setup finite_Collect ("finite (Collect P)") =
-  {* K Set_Comprehension_Pointfree.simproc *}
-
-(* FIXME: move to Set theory*)
-setup {*
-  Code_Preproc.map_pre (fn ss => ss addsimprocs
-    [Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}],
-    proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}])
-*}
+simproc_setup finite_Collect ("finite (Collect P)") = {* K Set_Comprehension_Pointfree.simproc *}
 
 lemma finite_induct [case_names empty insert, induct set: finite]:
   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
diff -r bed063d0c526 -r 9979d64b8016 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Oct 10 10:47:21 2012 +0200
+++ b/src/HOL/Product_Type.thy	Wed Oct 10 10:47:43 2012 +0200
@@ -1117,6 +1117,17 @@
 qed
 
 
+subsection {* Simproc for rewriting a set comprehension into a pointfree expression *}
+
+ML_file "Tools/set_comprehension_pointfree.ML"
+
+setup {*
+  Code_Preproc.map_pre (fn ss => ss addsimprocs
+    [Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}],
+    proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}])
+*}
+
+
 subsection {* Inductively defined sets *}
 
 ML_file "Tools/inductive_set.ML"