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