src/HOL/Tools/record_package.ML
changeset 9898 5f28e5b4c68e
parent 9705 8eecca293907
child 10008 61eb9f3aa92a
--- 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])];