# HG changeset patch
# User wenzelm
# Date 1014583653 -3600
# Node ID c1f3ff5feff174e941d1a4eafb7f855fde67ba30
# Parent  dbac8831d954a68579a9aeb9ca25e55df6b4092b
added using_thmss(_i);

diff -r dbac8831d954 -r c1f3ff5feff1 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Feb 24 21:47:01 2002 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Feb 24 21:47:33 2002 +0100
@@ -59,6 +59,8 @@
     (xstring * context attribute list) list) list -> state -> state
   val with_thmss_i: ((bstring * context attribute list) *
     (thm list * context attribute list) list) list -> state -> state
+  val using_thmss: ((xstring * context attribute list) list) list -> state -> state
+  val using_thmss_i: ((thm list * context attribute list) list) list -> state -> state
   val fix: (string list * string option) list -> state -> state
   val fix_i: (string list * typ option) list -> state -> state
   val assm: ProofContext.exporter
@@ -543,6 +545,26 @@
 end;
 
 
+(* using_thmss *)
+
+local
+
+fun gen_using_thmss f args state =
+  state
+  |> assert_backward
+  |> map_context_result (f (map (pair ("", [])) args))
+  |> (fn (st, named_facts) =>
+    let val (_, (_, ((result, (facts, thm)), f))) = find_goal st;
+    in st |> map_goal I (K ((result, (facts @ flat (map snd named_facts), thm)), f)) end);
+
+in
+
+val using_thmss = gen_using_thmss ProofContext.have_thmss;
+val using_thmss_i = gen_using_thmss ProofContext.have_thmss_i;
+
+end;
+
+
 (* fix *)
 
 fun gen_fix f xs state =