# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1254474621 -7200
# Node ID 1585a60b076d56b5f7171f7a56917fc16c5eb596
# Parent  4826ad24f772e270465730338a075bca5b07e4e0# Parent  1a92820a5b85fd5988d2df5af81747dbad39f91b
Merged

diff -r 4826ad24f772 -r 1585a60b076d QuotMain.thy
--- a/QuotMain.thy	Fri Oct 02 11:09:33 2009 +0200
+++ b/QuotMain.thy	Fri Oct 02 11:10:21 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"