src/Pure/Isar/attrib.ML
changeset 45491 3c9aff74fb58
parent 45390 e29521ef9059
child 45493 12453fd8dcff
     1.1 --- a/src/Pure/Isar/attrib.ML	Mon Nov 14 17:48:26 2011 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon Nov 14 19:27:42 2011 +0100
     1.3 @@ -25,7 +25,6 @@
     1.4      (('c * 'a list) * ('b * 'a list) list) list ->
     1.5      (('c * 'att list) * ('fact * 'att list) list) list
     1.6    val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
     1.7 -  val crude_closure: Proof.context -> src -> src
     1.8    val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
     1.9    val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
    1.10      theory -> theory
    1.11 @@ -142,19 +141,6 @@
    1.12    |> fst |> maps snd;
    1.13  
    1.14  
    1.15 -(* crude_closure *)
    1.16 -
    1.17 -(*Produce closure without knowing facts in advance! The following
    1.18 -  works reasonably well for attribute parsers that do not peek at the
    1.19 -  thm structure.*)
    1.20 -
    1.21 -fun crude_closure ctxt src =
    1.22 - (try (fn () =>
    1.23 -    Thm.apply_attribute (attribute_i (Proof_Context.theory_of ctxt) src)
    1.24 -      (Context.Proof ctxt, Drule.asm_rl)) ();
    1.25 -  Args.closure src);
    1.26 -
    1.27 -
    1.28  (* attribute setup *)
    1.29  
    1.30  fun syntax scan = Args.syntax "attribute" scan;