diff -r 0370493040f3 -r 5fe163543bb8 QuotMain.thy
--- a/QuotMain.thy	Mon Oct 12 13:58:31 2009 +0200
+++ b/QuotMain.thy	Mon Oct 12 14:30:50 2009 +0200
@@ -3,6 +3,7 @@
 uses ("quotient.ML")
 begin
 
+
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -145,6 +146,7 @@
 
 use "quotient.ML"
 
+
 ML {*
 val no_vars = Thm.rule_attribute (fn context => fn th =>
   let
@@ -223,7 +225,7 @@
 
 text {* information about map-functions for type-constructor *}
 ML {*
-type typ_info = {mapfun: string}
+type typ_info = {mapfun: string, relfun: string}
 
 local
   structure Data = TheoryDataFun
@@ -240,9 +242,9 @@
 
 (* mapfuns for some standard types *)
 setup {*
-  update @{type_name "list"} {mapfun = @{const_name "map"}} #> 
-  update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}} #> 
-  update @{type_name "fun"}  {mapfun = @{const_name "fun_map"}}
+  update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #> 
+  update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = "???"} #> 
+  update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
 *}
 
 ML {* lookup @{theory} @{type_name list} *}
@@ -285,7 +287,7 @@
 *}
 
 ML {*
-  get_fun repF @{typ t} @{typ qt} @{context} @{typ "t * nat"}
+  get_fun repF @{typ t} @{typ qt} @{context} @{typ "((t \<Rightarrow> t) list) * nat"}
   |> fst
   |> Syntax.string_of_term @{context}
   |> writeln
@@ -298,6 +300,32 @@
   |> writeln
 *}
 
+(*
+ML {*
+fun tyRel ty rty rel lthy =
+  if ty = rty 
+  then rel
+  else (case ty of
+         Type (s, tys) => 
+            (case (lookup (ProofContext.theory_of lthy) s) of
+               SOME (info) => list_comb (Const (#relfun info, ?????), map (tyRel ???) tys)
+               NONE  => (op =):: tys
+            )
+        | _ => (op =):: ty)
+*}
+
+ML {*
+
+fun regularise trm \<Rightarrow> new_trm 
+  (case trm of
+     ??
+  )
+*}
+
+fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
+  trm == new_trm
+*)
+
 text {* produces the definition for a lifted constant *}
 ML {*
 fun get_const_def nconst oconst rty qty lthy =