--- a/QuotMain.thy	Tue Oct 13 09:26:19 2009 +0200
+++ b/QuotMain.thy	Tue Oct 13 11:03:55 2009 +0200
@@ -300,12 +300,8 @@
   |> writeln
 *}
 
-ML {* op --> *}
-ML {* op ---> *}
-term FUN_REL
-term LIST_REL
-
-ML {* @{const_name "op ="} *}
+text {* tyRel takes a type and builds a relation that a quantifier over this
+  type needs to respect. *}
 ML {*
 fun tyRel ty rty rel lthy =
   if ty = rty then rel
@@ -324,16 +320,46 @@
         | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool}))
 *}
 
+definition
+  "x IN p ==> (Babs p m x = m x)"
+
+print_theorems
+thm Babs_def
+ML {* type_of @{term Babs } *}
 ML {*
   cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context})
 *}
-
-(* ML {*
+ML {* type_of @{term Respects } *}
 
-fun regularise trm \<Rightarrow> new_trm 
-  (case trm of
-     ??
-  )
+ML {*
+(* trm \<Rightarrow> new_trm *)
+fun regularise trm rty rel lthy =
+  case trm of
+    Abs (x, T, t) =>
+      if T = rty then let
+        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+        val v = Free (x', rty);
+        val t' = subst_bound (v, t);
+        val rec_term = regularise t' rty rel lthy2;
+        val lam_term = Term.lambda_name (x, v) rec_term;
+        val sub_res_term = tyRel T rty rel lthy;
+        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
+        val res_term = respects $ sub_res_term;
+        val ty = fastype_of trm;
+        val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);
+        val rabs_term = rabs $ respects $ lam_term;
+      in
+        rabs_term
+      end else let
+        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+        val v = Free (x', rty);
+        val t' = subst_bound (v, t);
+        val rec_term = regularise t' rty rel lthy2;
+      in
+        Term.lambda_name (x, v) rec_term
+      end
+  | _ => trm
+
 *}
 
 fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
@@ -1138,12 +1164,6 @@
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
 
-definition
-  "x IN p ==> (Babs p m x = m x)"
-
-print_theorems
-thm Babs_def
-
 lemma "(Ball (Respects ((op \<approx>) ===> (op =)))
          (((REP_fset ---> id) ---> id)
              (((ABS_fset ---> id) ---> id)