# HG changeset patch # User wenzelm # Date 1010693026 -3600 # Node ID 3d6684b5e4779870ebc4beab5554a3a77abcf9de # Parent 7bffaadc581e02c0294bd91f01550915af0fbc8f tuned; diff -r 7bffaadc581e -r 3d6684b5e477 src/Pure/Isar/isar_thy.ML --- 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 *)