# HG changeset patch
# User wenzelm
# Date 1281541024 -7200
# Node ID 3f4fadad94973451cd74bf5e2a3035d82d7b5335
# Parent  6551e310e7cbd165683ab7ca655c4f290e78ac26
removed obsolete Proof.get_thmss_cmd (cf. Attrib.eval_thms);

diff -r 6551e310e7cb -r 3f4fadad9497 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Aug 11 17:31:56 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Aug 11 17:37:04 2010 +0200
@@ -60,7 +60,6 @@
   val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
   val chain: state -> state
   val chain_facts: thm list -> state -> state
-  val get_thmss_cmd: state -> (Facts.ref * Attrib.src list) list -> thm list
   val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
   val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
   val from_thmss: ((thm list * attribute list) list) list -> state -> state
@@ -679,8 +678,6 @@
 
 val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
 
-fun get_thmss_cmd state srcs = the_facts (note_thmss_cmd [((Binding.empty, []), srcs)] state);
-
 end;