# HG changeset patch
# User wenzelm
# Date 1217874460 -7200
# Node ID f76b87a9d27cce28608ed98be96cd8a9339b921e
# Parent  aaf08262b177b46ad8c6b46befc887c5dbde32ef
removed obsolete apply_theorems(_i);

diff -r aaf08262b177 -r f76b87a9d27c src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Aug 04 20:27:39 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Aug 04 20:27:40 2008 +0200
@@ -16,8 +16,6 @@
   val oracle: bstring -> string -> string * Position.T -> theory -> theory
   val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
   val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
-  val apply_theorems: (Facts.ref * Attrib.src list) list -> theory -> thm list * theory
-  val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
   val declaration: string * Position.T -> local_theory -> local_theory
   val simproc_setup: string -> string list -> string * Position.T -> string list ->
     local_theory -> local_theory
@@ -199,15 +197,6 @@
     (snd oo (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded) args;
 
 
-(* facts *)
-
-fun apply_theorems args thy =
-  let val facts = Attrib.map_facts (Attrib.attribute thy) [(("", []), args)]
-  in apfst (maps snd) (PureThy.note_thmss_cmd "" facts thy) end;
-
-fun apply_theorems_i args = apfst (maps snd) o PureThy.note_thmss "" [(("", []), args)];
-
-
 (* declarations *)
 
 fun declaration (txt, pos) =