--- a/QuotMain.thy	Fri Oct 23 18:20:06 2009 +0200
+++ b/QuotMain.thy	Sat Oct 24 01:33:29 2009 +0200
@@ -3,8 +3,16 @@
 uses ("quotient.ML")
 begin
 
-ML {* Pretty.writeln *}
-ML {*  LocalTheory.theory_result *}
+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"
@@ -150,12 +158,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} *}
 
@@ -208,8 +216,10 @@
     (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
   end
 
-  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))
+  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 mk_identity ty = Abs ("", ty, Bound 0)