--- a/src/HOL/Tools/record_package.ML Mon Nov 16 11:12:59 1998 +0100
+++ b/src/HOL/Tools/record_package.ML Mon Nov 16 11:13:28 1998 +0100
@@ -76,7 +76,7 @@
fun prove_simp thy tacs simps =
let
val sign = Theory.sign_of thy;
- val ss = Simplifier.addsimps (HOL_basic_ss, map Attribute.thm_of simps);
+ val ss = Simplifier.addsimps (HOL_basic_ss, Attribute.thms_of simps);
fun prove goal =
Attribute.tthm_of
@@ -523,7 +523,7 @@
thy
|> field_type_defs fieldT_specs;
- val datatype_simps = map Attribute.tthm_of simps;
+ val datatype_simps = Attribute.tthms_of simps;
(* 2nd stage: defs_thy *)