# HG changeset patch # User wenzelm # Date 1030461944 -7200 # Node ID bb3e8a86d610ecf406d9862429e4917b85436cc4 # Parent 44efea0e21fa54bd54087f6c71e3479288869a26 thms_containing: allow "_" in specification; diff -r 44efea0e21fa -r bb3e8a86d610 doc-src/IsarRef/pure.tex --- a/doc-src/IsarRef/pure.tex Tue Aug 27 17:24:41 2002 +0200 +++ b/doc-src/IsarRef/pure.tex Tue Aug 27 17:25:44 2002 +0200 @@ -1390,9 +1390,9 @@ \item [$\isarkeyword{thms_containing}~\vec t$] retrieves facts from the theory or proof context containing all of the constants or variables occurring in - terms $\vec t$. Note that giving the empty list yields \emph{all} currently - known facts. An optional limit for the number printed facts may be given; - the default is 40. + terms $\vec t$ (which may contain occurrences of ``$\_$''). Note that + giving the empty list yields \emph{all} currently known facts. An optional + limit for the number printed facts may be given; the default is 40. \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts, using Isabelle's graph browser tool (see also \cite{isabelle-sys}). diff -r 44efea0e21fa -r bb3e8a86d610 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Aug 27 17:24:41 2002 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Aug 27 17:25:44 2002 +0200 @@ -552,28 +552,29 @@ local -fun gen_read read app is_pat schematic (ctxt as Context {defs = (_, _, used, _), ...}) s = +fun gen_read read app is_pat dummies schematic (ctxt as Context {defs = (_, _, used, _), ...}) s = (transform_error (read (syn_of ctxt) (sign_of ctxt) (def_type ctxt is_pat, def_sort ctxt, used)) s handle TERM (msg, _) => raise CONTEXT (msg, ctxt) | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt)) |> app (intern_skolem ctxt) |> app (if is_pat then I else norm_term ctxt schematic) - |> app (if is_pat then prepare_dummies else (reject_dummies ctxt)); + |> app (if is_pat then prepare_dummies else if dummies then I else reject_dummies ctxt); in -val read_termTs = gen_read (read_def_termTs false) (apfst o map) false false; -val read_termT_pats = #1 oo gen_read (read_def_termTs false) (apfst o map) true false; +val read_termTs = gen_read (read_def_termTs false) (apfst o map) false false false; +val read_termT_pats = #1 oo gen_read (read_def_termTs false) (apfst o map) true false false; fun read_term_pats T ctxt pats = read_termT_pats ctxt (map (rpair T) pats); val read_prop_pats = read_term_pats propT; -val read_term = gen_read (read_term_sg true) I false false; -val read_prop = gen_read (read_prop_sg true) I false false; -val read_prop_schematic = gen_read (read_prop_sg true) I false true; -val read_terms = gen_read (read_terms_sg true) map false false; -val read_props = gen_read (read_props_sg true) map false; +val read_term = gen_read (read_term_sg true) I false false false; +val read_term_dummies = gen_read (read_term_sg true) I false true false; +val read_prop = gen_read (read_prop_sg true) I false false false; +val read_prop_schematic = gen_read (read_prop_sg true) I false false true; +val read_terms = gen_read (read_terms_sg true) map false false false; +val read_props = gen_read (read_props_sg true) map false false; end; @@ -1409,7 +1410,7 @@ map (Pretty.quote o prt_term o Syntax.free) xs))]; val (cs, xs) = foldl (FactIndex.index_term (is_known ctxt)) - (([], []), map (read_term ctxt) ss); + (([], []), map (read_term_dummies ctxt) ss); val empty_idx = Library.null cs andalso Library.null xs; val header = diff -r 44efea0e21fa -r bb3e8a86d610 src/Pure/fact_index.ML --- a/src/Pure/fact_index.ML Tue Aug 27 17:24:41 2002 +0200 +++ b/src/Pure/fact_index.ML Tue Aug 27 17:25:44 2002 +0200 @@ -29,7 +29,7 @@ | add_frees _ (_, xs) = xs; fun index_term pred ((cs, xs), t) = - (Term.add_term_consts (t, cs), add_frees pred (t, xs)); + (Term.add_term_consts (t, cs) \ Term.dummy_patternN, add_frees pred (t, xs)); fun index_thm pred (idx, th) = let val {hyps, prop, ...} = Thm.rep_thm th