# HG changeset patch
# User wenzelm
# Date 911211208 -3600
# Node ID 92ba560f39ab57158fbc6d3985f28b6f67321ced
# Parent  d3ecef6b5682d03f1aafad5da10e0a44a8f71678
Attribute.thms_of;

diff -r d3ecef6b5682 -r 92ba560f39ab src/HOL/Tools/record_package.ML
--- 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 *)