# HG changeset patch
# User wenzelm
# Date 1450175668 -3600
# Node ID e8447e9eb574233825dd26d72e02c1c1a71aca53
# Parent  2c79790d270db445ca55a203a3a1ffb2a6ced565
unused;

diff -r 2c79790d270d -r e8447e9eb574 src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Mon Dec 14 14:05:31 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML	Tue Dec 15 11:34:28 2015 +0100
@@ -13,7 +13,6 @@
   val tag_free_thm: thm -> thm
   val is_free_thm: thm -> bool
   val dummy_free_thm: thm
-  val free_aware_rule_attribute: thm list -> (Context.generic -> thm -> thm) -> Thm.attribute
   val wrap_attribute: {handle_all_errs : bool, declaration : bool} ->
     Binding.binding -> theory -> theory
   val read: Proof.context -> Token.src -> Method.text
@@ -77,11 +76,6 @@
 
 fun is_free_thm thm = Properties.defined (Thm.get_tags thm) free_thmN;
 
-fun free_aware_rule_attribute args f =
-  Thm.rule_attribute (fn context => fn thm =>
-    if exists is_free_thm (thm :: args) then dummy_free_thm
-    else f context thm);
-
 fun free_aware_attribute thy {handle_all_errs, declaration} src (context, thm) =
   let
     val src' = map Token.init_assignable src;