diff -r f2565006dc5a -r 1a92820a5b85 QuotMain.thy
--- a/QuotMain.thy	Wed Sep 30 16:57:09 2009 +0200
+++ b/QuotMain.thy	Thu Oct 01 16:10:14 2009 +0200
@@ -318,6 +318,7 @@
 end
 *}
 
+
 section {* various tests for quotient types*}
 datatype trm =
   var  "nat"
@@ -391,9 +392,10 @@
 type typ_info = {mapfun: string}
 
 local
-  structure Data = GenericDataFun
+  structure Data = TheoryDataFun
   (type T = typ_info Symtab.table
    val empty = Symtab.empty
+   val copy = I
    val extend = I
    fun merge _ = Symtab.merge (K true))
 in
@@ -404,12 +406,12 @@
 
 (* mapfuns for some standard types *)
 setup {*
-    Context.theory_map (update @{type_name "list"} {mapfun = @{const_name "map"}})
- #> Context.theory_map (update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}})
- #> Context.theory_map (update @{type_name "fun"}  {mapfun = @{const_name "fun_map"}})
+  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"}}
 *}
 
-ML {* lookup (Context.Proof @{context}) @{type_name list} *}
+ML {* lookup @{theory} @{type_name list} *}
 
 ML {*
 datatype flag = absF | repF
@@ -426,7 +428,7 @@
     val nty = Type (s, ntys)
     val ftys = map (op -->) tys
   in
-   (case (lookup (Context.Proof lthy) s) of
+   (case (lookup (ProofContext.theory_of lthy) s) of
       SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty))
     | NONE      => raise ERROR ("no map association for type " ^ s))
   end
@@ -521,7 +523,6 @@
 term VR
 term AP
 
-
 text {* a test with functions *}
 datatype 'a t' =
   vr' "string"