# HG changeset patch
# User wenzelm
# Date 968352918 -7200
# Node ID 5f28e5b4c68ee9e5f3c0e7f4e594e1b02ea76750
# Parent  3a50d71323a805a807127f3ef1d529f0a0e5fa53
tuned;

diff -r 3a50d71323a8 -r 5f28e5b4c68e 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])];