# HG changeset patch
# User wenzelm
# Date 1449683146 -3600
# Node ID 93d0af296c2fa458435485110dce010a3373ec20
# Parent  1b67b7b02395cc65642b659e4aea0498a32b3bb0
unused;

diff -r 1b67b7b02395 -r 93d0af296c2f src/HOL/Eisbach/method_closure.ML
--- 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
diff -r 1b67b7b02395 -r 93d0af296c2f src/Pure/Isar/attrib.ML
--- 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