# HG changeset patch
# User wenzelm
# Date 1014583621 -3600
# Node ID dbac8831d954a68579a9aeb9ca25e55df6b4092b
# Parent  6ffd206f93ee5e0f8a50b32647c314e951eb190a
added using_facts;

diff -r 6ffd206f93ee -r dbac8831d954 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Sun Feb 24 21:45:57 2002 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Sun Feb 24 21:47:01 2002 +0100
@@ -56,6 +56,9 @@
   val with_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
   val with_facts_i: (thm * Proof.context attribute list) list list
     -> ProofHistory.T -> ProofHistory.T
+  val using_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
+  val using_facts_i: (thm * Proof.context attribute list) list list
+    -> ProofHistory.T -> ProofHistory.T
   val chain: ProofHistory.T -> ProofHistory.T
   val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T
   val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T
@@ -314,6 +317,13 @@
 val from_facts_i = chain_thmss (local_thmss_i Proof.have_thmss_i);
 val with_facts = chain_thmss (local_thmss Proof.with_thmss);
 val with_facts_i = chain_thmss (local_thmss_i Proof.with_thmss_i);
+
+fun using_facts args = ProofHistory.apply (fn state =>
+  Proof.using_thmss (map (map (apsnd (map
+    (Attrib.local_attribute (Proof.theory_of state))))) args) state);
+
+val using_facts_i = ProofHistory.apply o Proof.using_thmss_i o map (map (apfst single));
+
 val chain = ProofHistory.apply Proof.chain;