# HG changeset patch
# User berghofe
# Date 1194947433 -3600
# Node ID 1d8ebaf5f211a5096e9e2e21e18f5caff0425b32
# Parent  02884a4e1ac66fb70f5642c378bd1aff863042ee
to_pred and to_set now save induction and case rule tags.

diff -r 02884a4e1ac6 -r 1d8ebaf5f211 src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Mon Nov 12 23:08:12 2007 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Tue Nov 13 10:50:33 2007 +0100
@@ -340,7 +340,8 @@
     Thm.instantiate ([], insts) |>
     Simplifier.full_simplify (HOL_basic_ss addsimprocs
       [to_pred_simproc (mem_Collect_eq :: split_conv :: to_pred_simps)]) |>
-    eta_contract_thm (is_pred pred_arities)
+    eta_contract_thm (is_pred pred_arities) |>
+    RuleCases.save thm
   end;
 
 val to_pred_att = Thm.rule_attribute o to_pred;
@@ -367,9 +368,11 @@
            (HOLogic.mk_tuple' ps T (map Bound (length ps downto 0)), x'))))
       end) fs
   in
+    thm |>
+    Thm.instantiate ([], insts) |>
     Simplifier.full_simplify (HOL_basic_ss addsimps to_set_simps
-        addsimprocs [strong_ind_simproc pred_arities])
-      (Thm.instantiate ([], insts) thm)
+        addsimprocs [strong_ind_simproc pred_arities]) |>
+    RuleCases.save thm
   end;
 
 val to_set_att = Thm.rule_attribute o to_set;