--- a/src/HOL/Eisbach/method_closure.ML Wed Dec 09 18:28:28 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML Wed Dec 09 18:45:46 2015 +0100
@@ -77,9 +77,6 @@
fun is_free_thm thm = Properties.defined (Thm.get_tags thm) free_thmN;
-fun is_free_fact [thm] = is_free_thm thm
- | is_free_fact _ = false;
-
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
--- a/src/Pure/Isar/attrib.ML Wed Dec 09 18:28:28 2015 +0100
+++ b/src/Pure/Isar/attrib.ML Wed Dec 09 18:45:46 2015 +0100
@@ -19,7 +19,6 @@
val check_src: Proof.context -> Token.src -> Token.src
val attribs: Token.src list context_parser
val opt_attribs: Token.src list context_parser
- val markup_extern: Proof.context -> string -> Markup.T * xstring
val pretty_attribs: Proof.context -> Token.src list -> Pretty.T list
val pretty_binding: Proof.context -> binding -> string -> Pretty.T list
val attribute: Proof.context -> Token.src -> attribute