--- 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 *})

--- a/QuotMain.thy	Fri Nov 06 19:43:09 2009 +0100
+++ b/QuotMain.thy	Mon Nov 09 13:47:46 2009 +0100
@@ -495,24 +495,23 @@
         | Type (s, tys) => get_fun_aux s (map (get_fun_noexchange flag (rty, qty) lthy) tys)
         | _ => raise ERROR ("no type variables"))
 end
-*}
-
-ML {*
-fun old_get_fun flag rty qty lthy ty =
-  get_fun_noexchange flag (rty, qty) lthy ty 
+fun get_fun_noex flag (rty, qty) lthy ty =
+  fst (get_fun_noexchange flag (rty, qty) lthy ty)
 *}
 
 ML {*
 fun find_matching_types rty ty =
-  let val (s, tys) = dest_Type ty in
-    if Type.raw_instance (Logic.varifyT ty, rty)
-    then [ty]
-    else flat (map (find_matching_types rty) tys)
-  end
+  if Type.raw_instance (Logic.varifyT ty, rty)
+  then [ty]
+  else
+    let val (s, tys) = dest_Type ty in
+    flat (map (find_matching_types rty) tys)
+    end
+    handle _ => []
 *}
 
 ML {*
-fun get_fun_new flag rty qty lthy ty =
+fun get_fun_new flag (rty, qty) lthy ty =
   let
     val tys = find_matching_types rty ty;
     val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;
@@ -534,20 +533,20 @@
 ML {* val ttt = term_of @{cterm "f :: bool list \<Rightarrow> nat list"} *}
 
 ML {*
-  fst (get_fun_noexchange absF (al, aq) @{context} (fastype_of ttt))
+  get_fun_noexchange absF (al, aq) @{context} (fastype_of ttt)
 *}
 ML {*
-  fst (get_fun_new absF al aq @{context} (fastype_of ttt))
+  get_fun_new absF al aq @{context} (fastype_of ttt)
 *}
 ML {*
   fun mk_abs tm =
     let
       val ty = fastype_of tm
-    in fst (get_fun_noexchange absF (al, aq) @{context} ty) $ tm end
+    in (get_fun_noexchange absF (al, aq) @{context} ty) $ tm end
   fun mk_repabs tm =
     let
       val ty = fastype_of tm
-    in fst (get_fun_noexchange repF (al, aq) @{context} ty) $ (mk_abs tm) end
+    in (get_fun_noexchange repF (al, aq) @{context} ty) $ (mk_abs tm) end
 *}
 ML {*
   cterm_of @{theory} (mk_repabs ttt)
@@ -602,11 +601,11 @@
   fun mk_abs tm =
     let
       val ty = fastype_of tm
-    in fst (get_fun_noexchange absF (rty, qty) lthy ty) $ tm end
+    in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end
   fun mk_repabs tm =
     let
       val ty = fastype_of tm
-    in fst (get_fun_noexchange repF (rty, qty) lthy ty) $ (mk_abs tm) end
+    in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ (mk_abs tm)) end
 
     fun is_constructor (Const (x, _)) = member (op =) constructors x
       | is_constructor _ = false;
@@ -937,11 +936,11 @@
   fun mk_rep tm =
     let
       val ty = exchange_ty lthy qty rty (fastype_of tm)
-    in fst (get_fun_noexchange repF (rty, qty) lthy ty) $ tm end;
+    in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ tm) end;
   fun mk_abs tm =
     let
       val ty = fastype_of tm
-    in fst (get_fun_noexchange absF (rty, qty) lthy ty) $ tm end
+    in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end
   val (l, ltl) = Term.strip_type ty;
   val nl = map absty l;
   val vs = map (fn _ => "x") l;