--- a/FSet.thy	Sun Oct 25 00:14:40 2009 +0200
+++ b/FSet.thy	Sun Oct 25 01:15:03 2009 +0200
@@ -590,7 +590,7 @@
 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *}
 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *}
 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *}
-ML {* val thm = @{thm spec[OF FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]],symmetric]} *}
+ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *}
 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *}
 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *}
 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
@@ -625,6 +625,7 @@
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 notation ( output) "Trueprop" ("#_" [1000] 1000)
 
+(*
 ML {*
   fun lift_theorem_fset_aux thm lthy =
     let
@@ -641,7 +642,9 @@
       nthm3
     end
 *}
+*)
 
+(*
 ML {* lift_theorem_fset_aux @{thm m1} @{context} *}
 ML {*
   fun lift_theorem_fset name thm lthy =
@@ -652,6 +655,7 @@
       lthy2
     end;
 *}
+*)
 
 (* These do not work without proper definitions to rewrite back *)
 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}