# HG changeset patch
# User wenzelm
# Date 1321295262 -3600
# Node ID 3c9aff74fb58450c5619559a0834d10573c5f253
# Parent  20c8c0cca555cc5f9d4e03ae07edde28448797c4
eliminated dead code;

diff -r 20c8c0cca555 -r 3c9aff74fb58 src/Pure/Isar/attrib.ML
--- 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;