src/HOL/SPARK/Tools/spark_vcs.ML
changeset 44653 6d8d09b90398
parent 44030 b63a6bc144cf
child 45359 157e74588c49
--- 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