--- a/src/Pure/thm.ML Thu Oct 28 22:12:08 2010 +0200
+++ b/src/Pure/thm.ML Thu Oct 28 22:23:11 2010 +0200
@@ -39,7 +39,6 @@
(*theorems*)
type thm
type conv = cterm -> thm
- type attribute = Context.generic * thm -> Context.generic * thm
val rep_thm: thm ->
{thy_ref: theory_ref,
tags: Properties.T,
@@ -350,9 +349,6 @@
type conv = cterm -> thm;
-(*attributes subsume any kind of rules or context modifiers*)
-type attribute = Context.generic * thm -> Context.generic * thm;
-
(*errors involving theorems*)
exception THM of string * int * thm list;