# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263392256 -3600
# Node ID 09ec51d50fc6327f175a60f7b463fad462543a34
# Parent  adadd069647283b6158039ae2df521d986f16648
Stored Termtab for constant information.

diff -r adadd0696472 -r 09ec51d50fc6 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Wed Jan 13 13:12:04 2010 +0100
+++ b/Quot/quotient_def.ML	Wed Jan 13 15:17:36 2010 +0100
@@ -50,7 +50,7 @@
   (* data storage *)
   fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
   val lthy'' = Local_Theory.declaration true
-                 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'
+                 (fn phi => qconsts_update_gen trm (qcinfo phi)) lthy'
 in
   ((trm, thm), lthy'')
 end
diff -r adadd0696472 -r 09ec51d50fc6 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Wed Jan 13 13:12:04 2010 +0100
+++ b/Quot/quotient_info.ML	Wed Jan 13 15:17:36 2010 +0100
@@ -19,8 +19,8 @@
   type qconsts_info = {qconst: term, rconst: term, def: thm}
   val transform_qconsts: morphism -> qconsts_info -> qconsts_info
   val qconsts_lookup: theory -> term -> qconsts_info     (* raises NotFound *)
-  val qconsts_update_thy: string -> qconsts_info -> theory -> theory
-  val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
+  val qconsts_update_thy: term -> qconsts_info -> theory -> theory
+  val qconsts_update_gen: term -> qconsts_info -> Context.generic -> Context.generic
   val qconsts_dest: theory -> qconsts_info list
   val print_qconstinfo: Proof.context -> unit
 
@@ -182,27 +182,27 @@
 type qconsts_info = {qconst: term, rconst: term, def: thm}
 
 structure QConstsData = Theory_Data
-  (type T = qconsts_info Symtab.table
-   val empty = Symtab.empty
+  (type T = qconsts_info Termtab.table
+   val empty = Termtab.empty
    val extend = I
-   val merge = Symtab.merge (K true))
+   val merge = Termtab.merge (K true))
 
 fun transform_qconsts phi {qconst, rconst, def} =
     {qconst = Morphism.term phi qconst,
      rconst = Morphism.term phi rconst,
      def = Morphism.thm phi def}
 
-fun qconsts_update_thy str qcinfo = QConstsData.map (Symtab.update (str, qcinfo))
-fun qconsts_update_gen str qcinfo = Context.mapping (qconsts_update_thy str qcinfo) I
+fun qconsts_update_thy const qcinfo = QConstsData.map (Termtab.update (const, qcinfo))
+fun qconsts_update_gen const qcinfo = Context.mapping (qconsts_update_thy const qcinfo) I
 
 fun qconsts_dest thy =
-  map snd (Symtab.dest (QConstsData.get thy))
+  map snd (Termtab.dest (QConstsData.get thy))
 
 (* FIXME / TODO : better implementation of the lookup datastructure *)
 (* for example symtabs to alist; or tables with string type key     *) 
 fun qconsts_lookup thy t =
   let
-    val smt = Symtab.dest (QConstsData.get thy);
+    val smt = Termtab.dest (QConstsData.get thy);
     val (name, qty) = dest_Const t
     fun matches (_, x) =
       let
@@ -227,7 +227,7 @@
            Syntax.pretty_term ctxt (prop_of def)])
 in
   QConstsData.get (ProofContext.theory_of ctxt)
-  |> Symtab.dest
+  |> Termtab.dest
   |> map (prt_qconst o snd)
   |> Pretty.big_list "quotient constants:" 
   |> Pretty.writeln