removed obsolete Proof.get_thmss_cmd (cf. Attrib.eval_thms);

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