--- a/QuotMain.thy	Sat Oct 24 08:09:40 2009 +0200
+++ b/QuotMain.thy	Sat Oct 24 08:24:26 2009 +0200
@@ -3,16 +3,8 @@
 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
+ML {* Pretty.writeln *}
+ML {*  LocalTheory.theory_result *}
 
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
@@ -158,12 +150,12 @@
 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"}}
+*}
 
-ML {* quotdata_lookup @{theory} *}
-setup {* quotdata_update_thy (@{typ nat}, @{typ bool}, @{term "True"})*}
-ML {* quotdata_lookup @{theory} *}
-
-ML {* print_quotdata @{context} *}
 
 ML {* maps_lookup @{theory} @{type_name list} *}
 
@@ -216,10 +208,8 @@
     (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
   end
 
-  val thy = ProofContext.theory_of lthy
-
-  fun get_const absF = (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))
-    | get_const repF = (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))
+  fun get_const absF = (Const ("FSet.ABS_" ^ qty_name, rty --> qty), (rty, qty))
+    | get_const repF = (Const ("FSet.REP_" ^ qty_name, qty --> rty), (qty, rty))
 
   fun mk_identity ty = Abs ("", ty, Bound 0)