--- 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;