--- a/QuotMain.thy	Wed Oct 14 09:50:13 2009 +0200
+++ b/QuotMain.thy	Wed Oct 14 11:23:55 2009 +0200
@@ -331,14 +331,26 @@
   "BAll (R :: 'a \<Rightarrow> prop) (P :: 'a \<Rightarrow> prop) \<equiv> (\<And>x. (PROP R x \<Longrightarrow> PROP P x))"*)
 
 
+ML {* exists *}
+ML {* mem *}
+
+ML {*
+fun needs_lift (rty as Type (rty_s, _)) ty =
+  case ty of
+    Type (s, tys) =>
+      (s = rty_s) orelse (exists (needs_lift rty) tys)
+  | _ => false
+
+*}
+
 ML {*
 (* trm \<Rightarrow> new_trm *)
 fun regularise trm rty rel lthy =
   case trm of
     Abs (x, T, t) =>
-      if T = rty then let
+      if (needs_lift rty T) then let
         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', rty);
+        val v = Free (x', T);
         val t' = subst_bound (v, t);
         val rec_term = regularise t' rty rel lthy2;
         val lam_term = Term.lambda_name (x, v) rec_term;
@@ -352,16 +364,16 @@
         rabs_term
       end else let
         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', rty);
+        val v = Free (x', fastype_of t);
         val t' = subst_bound (v, t);
         val rec_term = regularise t' rty rel lthy2;
       in
         Term.lambda_name (x, v) rec_term
       end
   | ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) =>
-      if T = rty then let
+      if (needs_lift rty T) then let
         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', rty);
+        val v = Free (x', T);
         val t' = subst_bound (v, t);
         val rec_term = regularise t' rty rel lthy2;
         val lam_term = Term.lambda_name (x, v) rec_term;
@@ -375,7 +387,7 @@
         rall_term
       end else let
         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', rty);
+        val v = Free (x', fastype_of t);
         val t' = subst_bound (v, t);
         val rec_term = regularise t' rty rel lthy2;
         val lam_term = Term.lambda_name (x, v) rec_term
@@ -383,9 +395,9 @@
         Const(@{const_name "All"}, at) $ lam_term
       end
   | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>
-      if T = rty then let
+      if (needs_lift rty T) then let
         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', rty);
+        val v = Free (x', T);
         val t' = subst_bound (v, t);
         val rec_term = regularise t' rty rel lthy2;
         val lam_term = Term.lambda_name (x, v) rec_term;
@@ -399,7 +411,7 @@
         rall_term
       end else let
         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', rty);
+        val v = Free (x', fastype_of t);
         val t' = subst_bound (v, t);
         val rec_term = regularise t' rty rel lthy2;
         val lam_term = Term.lambda_name (x, v) rec_term