# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1258584768 -3600
# Node ID 746b17e1d6d8b4268306a86e6f167f5b252b0e7c
# Parent  d3c7f6d19c7f461e24355e6e607c8b9743622945
fixed the storage of qconst definitions

diff -r d3c7f6d19c7f -r 746b17e1d6d8 IntEx.thy
--- a/IntEx.thy	Fri Nov 13 19:32:12 2009 +0100
+++ b/IntEx.thy	Wed Nov 18 23:52:48 2009 +0100
@@ -20,16 +20,23 @@
 where
   "ZERO \<equiv> (0::nat, 0::nat)"
 
+ML {* print_qconstinfo @{context} *}
+
+
 term ZERO
 thm ZERO_def
 
 ML {* prop_of @{thm ZERO_def} *}
 
+ML {* separate *}
+
 quotient_def 
   ONE::"my_int"
 where
   "ONE \<equiv> (1::nat, 0::nat)"
 
+ML {* print_qconstinfo @{context} *}
+
 term ONE
 thm ONE_def
 
@@ -43,6 +50,7 @@
 where
   "PLUS \<equiv> my_plus"
 
+term my_plus
 term PLUS
 thm PLUS_def
 
diff -r d3c7f6d19c7f -r 746b17e1d6d8 quotient_def.ML
--- a/quotient_def.ML	Fri Nov 13 19:32:12 2009 +0100
+++ b/quotient_def.ML	Wed Nov 18 23:52:48 2009 +0100
@@ -139,8 +139,10 @@
   val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy
 
   val nconst_str = Binding.name_of nconst_bname
-  val qc_info = {qconst = trm, rconst = rhs}
-  val lthy'' = qconsts_update nconst_str qc_info lthy'
+  val qcinfo = {qconst = trm, rconst = rhs}
+  val lthy'' = LocalTheory.declaration true
+                (fn phi => qconsts_update_generic nconst_str 
+                             (qconsts_transfer phi qcinfo)) lthy'
 in
   ((trm, thm), lthy'')
 end
diff -r d3c7f6d19c7f -r 746b17e1d6d8 quotient_info.ML
--- a/quotient_info.ML	Fri Nov 13 19:32:12 2009 +0100
+++ b/quotient_info.ML	Wed Nov 18 23:52:48 2009 +0100
@@ -17,9 +17,10 @@
   val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option
 
   type qconsts_info = {qconst: term, rconst: term}
+  val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
   val qconsts_lookup: theory -> string -> qconsts_info option
   val qconsts_update_thy: string -> qconsts_info -> theory -> theory    
-  val qconsts_update: string -> qconsts_info -> Proof.context -> Proof.context 
+  val qconsts_update_generic: string -> qconsts_info -> Context.generic -> Context.generic 
   val print_qconstinfo: Proof.context -> unit
 end;
 
@@ -137,17 +138,22 @@
    val extend = I
    val merge = Symtab.merge (K true))
 
+fun qconsts_transfer phi {qconst, rconst} =
+    {qconst = Morphism.term phi qconst,
+     rconst = Morphism.term phi rconst}
+
 val qconsts_lookup = Symtab.lookup o QConstsData.get
 
 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
-fun qconsts_update k qcinfo = ProofContext.theory (qconsts_update_thy k qcinfo)
+fun qconsts_update_generic k qcinfo = 
+      Context.mapping (qconsts_update_thy k qcinfo) I
 
 fun print_qconstinfo ctxt =
 let
   fun prt_qconst {qconst, rconst} = 
-      Pretty.block (Library.separate (Pretty.brk 2)
+      Pretty.block (separate (Pretty.brk 1)
           [Syntax.pretty_term ctxt qconst,
-           Pretty.str (" := "),
+           Pretty.str ":=",
            Syntax.pretty_term ctxt rconst])
 in
   QConstsData.get (ProofContext.theory_of ctxt)