# HG changeset patch
# User wenzelm
# Date 1433017092 -7200
# Node ID 9b7248379101eb6362b247b6ef30e7c2f4596426
# Parent  e487b83a9885f95ef5dd99fb5bc2ef934497fd02
unused;

diff -r e487b83a9885 -r 9b7248379101 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sat May 30 22:04:15 2015 +0200
+++ b/src/Pure/Pure.thy	Sat May 30 22:18:12 2015 +0200
@@ -186,10 +186,6 @@
     in th' end))\<close>
   "imported schematic variables"
 
-attribute_setup eta_long =
-  \<open>Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))\<close>
-  "put theorem into eta long beta normal form"
-
 attribute_setup atomize =
   \<open>Scan.succeed Object_Logic.declare_atomize\<close>
   "declaration of atomize rule"