--- a/src/Pure/Isar/attrib.ML Mon Nov 14 17:48:26 2011 +0100
+++ b/src/Pure/Isar/attrib.ML Mon Nov 14 19:27:42 2011 +0100
@@ -25,7 +25,6 @@
(('c * 'a list) * ('b * 'a list) list) list ->
(('c * 'att list) * ('fact * 'att list) list) list
val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
- val crude_closure: Proof.context -> src -> src
val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
theory -> theory
@@ -142,19 +141,6 @@
|> fst |> maps snd;
-(* crude_closure *)
-
-(*Produce closure without knowing facts in advance! The following
- works reasonably well for attribute parsers that do not peek at the
- thm structure.*)
-
-fun crude_closure ctxt src =
- (try (fn () =>
- Thm.apply_attribute (attribute_i (Proof_Context.theory_of ctxt) src)
- (Context.Proof ctxt, Drule.asm_rl)) ();
- Args.closure src);
-
-
(* attribute setup *)
fun syntax scan = Args.syntax "attribute" scan;