--- a/QuotMain.thy	Fri Oct 30 12:22:03 2009 +0100
+++ b/QuotMain.thy	Fri Oct 30 14:25:37 2009 +0100
@@ -903,19 +903,31 @@
   end
 *}
 
-text {* the proper way to do it *}
 ML {*
-  fun findabs rty tm =
+  fun findabs_all rty tm =
     case tm of
       Abs(_, T, b) =>
         let
           val b' = subst_bound ((Free ("x", T)), b);
-          val tys = findabs rty b'
+          val tys = findabs_all rty b'
           val ty = fastype_of tm
         in if needs_lift rty ty then (ty :: tys) else tys
         end
-    | f $ a => (findabs rty f) @ (findabs rty a)
-    | _ => []
+    | f $ a => (findabs_all rty f) @ (findabs_all rty a)
+    | _ => [];
+  fun findabs rty tm = distinct (op =) (findabs_all rty tm)
+*}
+
+
+ML {*
+  fun findaps_all rty tm =
+    case tm of
+      Abs(_, T, b) =>
+        findaps_all rty (subst_bound ((Free ("x", T)), b))
+    | (f $ a) => (findaps_all rty f @ findaps_all rty a)
+    | Free (_, (T as (Type (_, (_ :: _))))) => (if needs_lift rty T then [T] else [])
+    | _ => [];
+  fun findaps rty tm = distinct (op =) (findaps_all rty tm)
 *}
 
 ML {*