Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Attribute.thms_of;
authorwenzelm
Mon, 16 Nov 1998 11:13:28 +0100
changeset 5890 92ba560f39ab
parent 5889 d3ecef6b5682
child 5891 92e0f5e6fd17
Attribute.thms_of;
src/HOL/Tools/record_package.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle