thms_containing: allow "_" in specification;
authorwenzelm
Tue Aug 27 17:25:44 2002 +0200 (2002-08-27)
changeset 13542bb3e8a86d610
parent 13541 44efea0e21fa
child 13543 2b3c7e319d82
thms_containing: allow "_" in specification;
doc-src/IsarRef/pure.tex
src/Pure/Isar/proof_context.ML
src/Pure/fact_index.ML
     1.1 --- a/doc-src/IsarRef/pure.tex	Tue Aug 27 17:24:41 2002 +0200
     1.2 +++ b/doc-src/IsarRef/pure.tex	Tue Aug 27 17:25:44 2002 +0200
     1.3 @@ -1390,9 +1390,9 @@
     1.4    
     1.5  \item [$\isarkeyword{thms_containing}~\vec t$] retrieves facts from the theory
     1.6    or proof context containing all of the constants or variables occurring in
     1.7 -  terms $\vec t$.  Note that giving the empty list yields \emph{all} currently
     1.8 -  known facts.  An optional limit for the number printed facts may be given;
     1.9 -  the default is 40.
    1.10 +  terms $\vec t$ (which may contain occurrences of ``$\_$'').  Note that
    1.11 +  giving the empty list yields \emph{all} currently known facts.  An optional
    1.12 +  limit for the number printed facts may be given; the default is 40.
    1.13    
    1.14  \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts,
    1.15    using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
     2.1 --- a/src/Pure/Isar/proof_context.ML	Tue Aug 27 17:24:41 2002 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Aug 27 17:25:44 2002 +0200
     2.3 @@ -552,28 +552,29 @@
     2.4  
     2.5  local
     2.6  
     2.7 -fun gen_read read app is_pat schematic (ctxt as Context {defs = (_, _, used, _), ...}) s =
     2.8 +fun gen_read read app is_pat dummies schematic (ctxt as Context {defs = (_, _, used, _), ...}) s =
     2.9    (transform_error (read (syn_of ctxt)
    2.10        (sign_of ctxt) (def_type ctxt is_pat, def_sort ctxt, used)) s
    2.11      handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
    2.12      | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
    2.13    |> app (intern_skolem ctxt)
    2.14    |> app (if is_pat then I else norm_term ctxt schematic)
    2.15 -  |> app (if is_pat then prepare_dummies else (reject_dummies ctxt));
    2.16 +  |> app (if is_pat then prepare_dummies else if dummies then I else reject_dummies ctxt);
    2.17  
    2.18  in
    2.19  
    2.20 -val read_termTs = gen_read (read_def_termTs false) (apfst o map) false false;
    2.21 -val read_termT_pats = #1 oo gen_read (read_def_termTs false) (apfst o map) true false;
    2.22 +val read_termTs = gen_read (read_def_termTs false) (apfst o map) false false false;
    2.23 +val read_termT_pats = #1 oo gen_read (read_def_termTs false) (apfst o map) true false false;
    2.24  
    2.25  fun read_term_pats T ctxt pats = read_termT_pats ctxt (map (rpair T) pats);
    2.26  val read_prop_pats = read_term_pats propT;
    2.27  
    2.28 -val read_term = gen_read (read_term_sg true) I false false;
    2.29 -val read_prop = gen_read (read_prop_sg true) I false false;
    2.30 -val read_prop_schematic = gen_read (read_prop_sg true) I false true;
    2.31 -val read_terms = gen_read (read_terms_sg true) map false false;
    2.32 -val read_props = gen_read (read_props_sg true) map false;
    2.33 +val read_term = gen_read (read_term_sg true) I false false false;
    2.34 +val read_term_dummies = gen_read (read_term_sg true) I false true false;
    2.35 +val read_prop = gen_read (read_prop_sg true) I false false false;
    2.36 +val read_prop_schematic = gen_read (read_prop_sg true) I false false true;
    2.37 +val read_terms = gen_read (read_terms_sg true) map false false false;
    2.38 +val read_props = gen_read (read_props_sg true) map false false;
    2.39  
    2.40  end;
    2.41  
    2.42 @@ -1409,7 +1410,7 @@
    2.43            map (Pretty.quote o prt_term o Syntax.free) xs))];
    2.44  
    2.45      val (cs, xs) = foldl (FactIndex.index_term (is_known ctxt))
    2.46 -      (([], []), map (read_term ctxt) ss);
    2.47 +      (([], []), map (read_term_dummies ctxt) ss);
    2.48      val empty_idx = Library.null cs andalso Library.null xs;
    2.49  
    2.50      val header =
     3.1 --- a/src/Pure/fact_index.ML	Tue Aug 27 17:24:41 2002 +0200
     3.2 +++ b/src/Pure/fact_index.ML	Tue Aug 27 17:25:44 2002 +0200
     3.3 @@ -29,7 +29,7 @@
     3.4    | add_frees _ (_, xs) = xs;
     3.5  
     3.6  fun index_term pred ((cs, xs), t) =
     3.7 -  (Term.add_term_consts (t, cs), add_frees pred (t, xs));
     3.8 +  (Term.add_term_consts (t, cs) \ Term.dummy_patternN, add_frees pred (t, xs));
     3.9  
    3.10  fun index_thm pred (idx, th) =
    3.11    let val {hyps, prop, ...} = Thm.rep_thm th