diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Boogie/Tools/boogie_vcs.ML
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -19,14 +19,13 @@
 
 fun err_vcs () = error "undischarged Boogie verification conditions found"
 
-structure VCs = TheoryDataFun
+structure VCs = Theory_Data
 (
-  type T = (Term.term * bool) Symtab.table option
+  type T = (term * bool) Symtab.table option
   val empty = NONE
-  val copy = I
   val extend = I
-  fun merge _ (NONE, NONE) = NONE
-    | merge _ (_, _) = err_vcs ()
+  fun merge (NONE, NONE) = NONE
+    | merge _ = err_vcs ()
 )
 
 fun set vcs = VCs.map (fn