--- a/FSet.thy	Wed Nov 25 14:16:33 2009 +0100
+++ b/FSet.thy	Wed Nov 25 14:25:29 2009 +0100
@@ -397,7 +397,7 @@
 done
 
 lemma list_induct_part:
-  assumes a: "P (x :: 'a list) ([] :: 'a list)"
+  assumes a: "P (x :: 'a list) ([] :: 'c list)"
   assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"
   shows "P x l"
   apply (rule_tac P="P x" in list.induct)
@@ -412,58 +412,8 @@
 
 
 
-ML {*
-fun lambda_prs_conv1 ctxt quot ctrm =
-  case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
-  let
-    val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
-    val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);
-    val thy = ProofContext.theory_of ctxt;
-    val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
-    val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d];
-    val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
-    val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
-    val tac =
-      (compose_tac (false, lpi, 2)) THEN_ALL_NEW
-      (quotient_tac quot);
-    val gc = Drule.strip_imp_concl (cprop_of lpi);
-    val t = Goal.prove_internal [] gc (fn _ => tac 1)
-    val te = @{thm eq_reflection} OF [t]
-    val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te
-    val tl = Thm.lhs_of ts
-    val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));
-    val _ = tracing (Syntax.string_of_term @{context} (term_of tl));
-    val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm);
-    val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts);
-(*    val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
-  in
-    Conv.rewr_conv ti ctrm
-  end
-  handle _ => Conv.all_conv ctrm
-
-*}
-ML {*
-fun lambda_prs_conv ctxt quot ctrm =
-  case (term_of ctrm) of
-    (Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs (_, _, x)) =>
-      (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)
-      then_conv (lambda_prs_conv1 ctxt quot)) ctrm
-  | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
-  | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
-  | _ => Conv.all_conv ctrm
-*}
-
-ML {*
-fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
-  CONVERSION
-    (Conv.params_conv ~1 (fn ctxt =>
-       (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv
-          Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
-*}
-
-
 (* Construction site starts here *)
-lemma "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
+lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *})
 apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
@@ -539,7 +489,7 @@
 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *})
 apply (tactic {* lambda_prs_tac @{context} quot 1 *})
-ML_prf {* val t = applic_prs @{context} rty qty absrep @{typ "('b \<Rightarrow> 'a list \<Rightarrow> bool)"} *}
+ML_prf {* val t = applic_prs @{context} rty qty absrep @{typ "('b \<Rightarrow> 'c list \<Rightarrow> bool)"} *}
 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] [t]) 1 *})
 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
 done