diff -r 8f8652a8107f -r 2f289c1f6cf1 Nominal/Ex/ExPS8.thy
--- a/Nominal/Ex/ExPS8.thy	Sat Sep 11 05:56:49 2010 +0800
+++ b/Nominal/Ex/ExPS8.thy	Sun Sep 12 22:46:40 2010 +0800
@@ -58,15 +58,6 @@
 thm fun_pats.fsupp
 thm fun_pats.supp
 
-
-ML {*
-fun add_ss thms =
-  HOL_basic_ss addsimps thms
-
-fun symmetric thms = 
-  map (fn thm => thm RS @{thm sym}) thms
-*}
-
 lemma
   "(fv_exp x = supp x) \<and>
    (fv_fnclause xa = supp xa \<and> fv_b_lrb xa = supp_rel alpha_b_lrb xa) \<and>
@@ -92,7 +83,13 @@
   "fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb" and 
   "fv_b_fnclause xc = supp_rel alpha_b_fnclause xc" and
   "fv_b_lrb y = supp_rel alpha_b_lrb y"
-apply(induct "x::exp" and "y::fnclause" and xb and xc and xd and xe rule: fun_pats.inducts)
+thm fun_pats.inducts
+apply(induct rule: fun_pats.inducts(1)[where ?exp="x::exp"] 
+                   fun_pats.inducts(2)[where ?fnclause="y"]
+                   fun_pats.inducts(3)[where ?fnclauses="xb"]
+                   fun_pats.inducts(4)[where ?lrb="xc"] 
+                   fun_pats.inducts(5)[where ?lrbs="xd"]
+                   fun_pats.inducts(6)[where ?pat="xe"])
 thm fun_pats.inducts
 oops