--- 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;