diff -r 1cc7df9ff83b -r 6d8d09b90398 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Sep 02 16:20:09 2011 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Sep 02 17:57:37 2011 +0200
@@ -349,7 +349,7 @@
          map (rpair (mk_type thy prfx ty)) flds) fldtys
        in case get_type thy prfx s of
            NONE =>
-             Record.add_record true ([], Binding.name s) NONE
+             Record.add_record ([], Binding.name s) NONE
                (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
          | SOME rT =>
              (case get_record_info thy rT of