--- a/src/Pure/Isar/isar_thy.ML Thu Jan 10 16:09:26 2002 +0100
+++ b/src/Pure/Isar/isar_thy.ML Thu Jan 10 21:03:46 2002 +0100
@@ -318,12 +318,16 @@
(* theorems *)
+local
+
fun prep_thmss get attrib = map (fn ((name, more_srcs), th_srcs) =>
((name, map attrib more_srcs), map (fn (s, srcs) => (get s, map attrib srcs)) th_srcs));
fun flat_unnamed (x, ys) = (x, flat (map snd ys));
fun cond_kind k = if k = "" then [] else [Drule.kind k];
+in
+
fun global_have_thmss kind f args thy =
let
val args' = prep_thmss (PureThy.get_thms thy) (Attrib.global_attribute thy) args
@@ -360,6 +364,8 @@
val have_facts = ProofHistory.apply o local_have_thmss Proof.have_thmss o map Comment.ignore;
val have_facts_i = ProofHistory.apply o gen_have_thmss_i Proof.have_thmss o map Comment.ignore;
+end;
+
(* forward chaining *)