diff -r 0c1dcdefb515 -r 31f1ec832d39 Nominal-General/nominal_thmdecls.ML
--- a/Nominal-General/nominal_thmdecls.ML	Thu May 27 11:21:37 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML	Thu May 27 18:30:26 2010 +0200
@@ -47,13 +47,13 @@
   val merge = Item_Net.merge);
 
 structure EqvtRawData = Generic_Data
-( type T = thm Symtab.table;
-  val empty = Symtab.empty;
+( type T = thm Termtab.table;
+  val empty = Termtab.empty;
   val extend = I;
-  val merge = Symtab.merge (K true));
+  val merge = Termtab.merge (K true));
 
 val eqvts = Item_Net.content o EqvtData.get;
-val eqvts_raw = map snd o Symtab.dest o EqvtRawData.get;
+val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get;
 
 val get_eqvts_thms = eqvts o  Context.Proof;
 val get_eqvts_raw_thms = eqvts_raw o Context.Proof;
@@ -63,17 +63,17 @@
 
 fun add_raw_thm thm = 
   case prop_of thm of
-    Const ("==", _) $ _ $ Const (c, _) => EqvtRawData.map (Symtab.update (c, thm))
+    Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.update (c, thm)) 
   | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) 
 
 fun del_raw_thm thm = 
   case prop_of thm of
-    Const ("==", _) $ _ $ Const (c, _) => EqvtRawData.map (Symtab.delete c)
+    Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.delete c)
   | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) 
 
 fun is_eqvt ctxt trm =
   case trm of 
-    Const (c, _) => Symtab.defined (EqvtRawData.get (Context.Proof ctxt)) c
+    (c as Const _) => Termtab.defined (EqvtRawData.get (Context.Proof ctxt)) c
   | _ => raise TERM ("Term must be a constsnt.", [trm])