src/Pure/Pure.thy
changeset 60317 9b7248379101
parent 60093 c48d536231fe
child 60371 8a5cfdda1b98
--- 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"