tuned;
authorwenzelm
Thu, 07 Sep 2000 20:55:18 +0200
changeset 9898 5f28e5b4c68e
parent 9897 3a50d71323a8
child 9899 5a9081c3b869
tuned;
src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Sep 07 20:53:50 2000 +0200
+++ b/src/HOL/Tools/record_package.ML	Thu Sep 07 20:55:18 2000 +0200
@@ -829,7 +829,7 @@
           ("select_convs", sel_convs),
           ("update_convs", update_convs)]
       |> (#1 oo (PureThy.add_thms o map Thm.no_attributes))
-	  [("equality", equality)]
+          [("equality", equality)]
       |> (#1 oo PureThy.add_thmss)
         [(("simps", simps), [Simplifier.simp_add_global]),
          (("iffs", iffs), [iff_add_global])];