--- a/FSet.thy	Fri Nov 06 19:43:09 2009 +0100
+++ b/FSet.thy	Mon Nov 09 13:47:46 2009 +0100
@@ -345,6 +345,7 @@
 
 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
 
+
 ML {* map (lift_thm_fset @{context}) @{thms list.recs} *}
 ML {* map (lift_thm_fset @{context}) @{thms list.cases} *}
 
@@ -386,11 +387,7 @@
   val rt = build_repabs_term @{context} t_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
 *}
-
-ML {* val ttt = snd (dest_Free (term_of @{cpat "f :: ?'a list \<Rightarrow> ?'a list"})) *}
-ML {* old_get_fun repF @{typ "'a list"} @{typ "'a fset"} @{context} @{typ "'a list \<Rightarrow> 'a list"} *}
-
-prove rg
+prove {* Syntax.check_term @{context} rg *}
 apply(atomize(full))
 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})