--- a/QuotMain.thy	Mon Oct 12 14:30:50 2009 +0200
+++ b/QuotMain.thy	Mon Oct 12 15:47:27 2009 +0200
@@ -300,21 +300,35 @@
   |> writeln
 *}
 
-(*
+ML {* op --> *}
+ML {* op ---> *}
+term FUN_REL
+term LIST_REL
+
+ML {* @{const_name "op ="} *}
 ML {*
 fun tyRel ty rty rel lthy =
-  if ty = rty 
-  then rel
+  if ty = rty then rel
   else (case ty of
-         Type (s, tys) => 
+          Type (s, tys) =>
+            let
+              val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
+              val ty_out = ty --> ty --> @{typ bool};
+              val tys_out = tys_rel ---> ty_out;
+            in
             (case (lookup (ProofContext.theory_of lthy) s) of
-               SOME (info) => list_comb (Const (#relfun info, ?????), map (tyRel ???) tys)
-               NONE  => (op =):: tys
+               SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
+             | NONE  => Const (@{const_name "op ="}, ty --> ty --> @{typ bool})
             )
-        | _ => (op =):: ty)
+            end
+        | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool}))
 *}
 
 ML {*
+  cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context})
+*}
+
+(* ML {*
 
 fun regularise trm \<Rightarrow> new_trm 
   (case trm of