--- a/QuotMain.thy	Sun Oct 25 01:31:04 2009 +0200
+++ b/QuotMain.thy	Sun Oct 25 23:44:41 2009 +0100
@@ -3,17 +3,6 @@
 uses ("quotient.ML")
 begin
 
-definition 
-  EQ_TRUE 
-where
-  "EQ_TRUE X \<equiv> (X = True)"
-
-lemma test: "EQ_TRUE ?X"
-  unfolding EQ_TRUE_def
-  by (rule refl)
-
-thm test
-
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -155,14 +144,17 @@
 
 section {* type definition for the quotient type *}
 
+ML {* Toplevel.theory *}
+
 use "quotient.ML"
 
-(* mapfuns for some standard types *)
-setup {*
-  maps_update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #>
-  maps_update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #>
-  maps_update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
-*}
+declare [[map list = (map, LIST_REL)]]
+declare [[map * = (prod_fun, prod_rel)]]
+declare [[map "fun" = (fun_map, FUN_REL)]]
+
+ML {* maps_lookup @{theory} "List.list" *}
+ML {* maps_lookup @{theory} "*" *}
+ML {* maps_lookup @{theory} "fun" *}
 
 ML {*
 val no_vars = Thm.rule_attribute (fn context => fn th =>
@@ -175,6 +167,10 @@
 section {* lifting of constants *}
 
 ML {*
+
+*}
+
+ML {*
 (* calculates the aggregate abs and rep functions for a given type; 
    repF is for constants' arguments; absF is for constants;
    function types need to be treated specially, since repF and absF