# HG changeset patch
# User wenzelm
# Date 981056594 -3600
# Node ID 241cbdf4134e332c98e4d30a6857ef557aec23b8
# Parent  8f8ba41a5e7ae4b065ff6b680578bc389d0e5c8f
thms_containing: term args;

diff -r 8f8ba41a5e7a -r 241cbdf4134e doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Thu Feb 01 20:42:34 2001 +0100
+++ b/doc-src/IsarRef/pure.tex	Thu Feb 01 20:43:14 2001 +0100
@@ -1276,7 +1276,7 @@
 \railterm{thmdeps}
 
 \begin{rail}
-  thmscontaining (name * )
+  thmscontaining (term * )
   ;
   thmdeps thmrefs
   ;
@@ -1301,9 +1301,10 @@
   current theory context.  In interactive mode this actually refers to the
   theorems left by the last transaction; this allows to inspect the result of
   advanced definitional packages, such as $\isarkeyword{datatype}$.
-\item [$\isarkeyword{thms_containing}~\vec c$] retrieves theorems from the
-  theory context containing all of the constants $\vec c$.  Note that giving
-  the empty list yields \emph{all} theorems of the current theory.
+\item [$\isarkeyword{thms_containing}~\vec t$] retrieves theorems from the
+  theory context containing all of the constants occurring in the terms $\vec
+  t$.  Note that giving the empty list yields \emph{all} theorems of the
+  current theory.
 \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of theorems
   and lemmas, using Isabelle's graph browser tool (see also
   \cite{isabelle-sys}).
diff -r 8f8ba41a5e7a -r 241cbdf4134e src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Thu Feb 01 20:42:34 2001 +0100
+++ b/src/Pure/Interface/proof_general.ML	Thu Feb 01 20:43:14 2001 +0100
@@ -13,7 +13,7 @@
   val try_update_thy_only: string -> unit
   val inform_file_processed: string -> unit
   val inform_file_retracted: string -> unit
-  val thms_containing: xstring list -> unit
+  val thms_containing: string list -> unit
   val help: unit -> unit
   val show_context: unit -> theory
   val kill_goal: unit -> unit
@@ -180,7 +180,11 @@
 
 (* misc commands for ProofGeneral/isa *)
 
-fun thms_containing cs = ThmDatabase.print_thms_containing (the_context ()) cs;
+fun thms_containing ss =
+  let
+    val thy = the_context ();
+    fun read_term s = Thm.term_of (Thm.read_cterm (Theory.sign_of thy) (s, TypeInfer.logicT));
+  in ThmDatabase.print_thms_containing thy (map read_term ss) end;
 
 val welcome = priority o Session.welcome;
 val help = welcome;
diff -r 8f8ba41a5e7a -r 241cbdf4134e src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Feb 01 20:42:34 2001 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Feb 01 20:43:14 2001 +0100
@@ -50,7 +50,7 @@
   val print_trans_rules: Toplevel.transition -> Toplevel.transition
   val print_methods: Toplevel.transition -> Toplevel.transition
   val print_antiquotations: Toplevel.transition -> Toplevel.transition
-  val print_thms_containing: xstring list -> Toplevel.transition -> Toplevel.transition
+  val print_thms_containing: string list -> Toplevel.transition -> Toplevel.transition
   val thm_deps: (string * Args.src list) list -> Toplevel.transition -> Toplevel.transition
   val print_binds: Toplevel.transition -> Toplevel.transition
   val print_lthms: Toplevel.transition -> Toplevel.transition
@@ -195,8 +195,9 @@
 
 val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
 
-fun print_thms_containing cs = Toplevel.unknown_theory o
-  Toplevel.keep (fn state => ThmDatabase.print_thms_containing (Toplevel.theory_of state) cs);
+fun print_thms_containing ss = Toplevel.unknown_theory o Toplevel.keep (fn state =>
+  ThmDatabase.print_thms_containing (Toplevel.theory_of state)
+    (map (ProofContext.read_term (Toplevel.context_of state)) ss));
 
 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state)));
diff -r 8f8ba41a5e7a -r 241cbdf4134e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Feb 01 20:42:34 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Feb 01 20:43:14 2001 +0100
@@ -539,8 +539,8 @@
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
 
 val thms_containingP =
-  OuterSyntax.improper_command "thms_containing" "print theorems containing all given constants"
-    K.diag (Scan.repeat P.xname >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
+  OuterSyntax.improper_command "thms_containing" "print theorems containing certain constants"
+    K.diag (Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
 
 val thm_depsP =
   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
diff -r 8f8ba41a5e7a -r 241cbdf4134e src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Thu Feb 01 20:42:34 2001 +0100
+++ b/src/Pure/Thy/thm_database.ML	Thu Feb 01 20:43:14 2001 +0100
@@ -29,7 +29,7 @@
   val ml_store_thm: string * thm -> unit
   val ml_store_thms: string * thm list -> unit
   val is_ml_identifier: string -> bool
-  val print_thms_containing: theory -> xstring list -> unit
+  val print_thms_containing: theory -> term list -> unit
 end;
 
 structure ThmDatabase: THM_DATABASE =
@@ -95,22 +95,34 @@
 
 (** retrieve theorems **)
 
-(*get theorems that contain all of given constants*)
-fun thms_containing_thy thy raw_consts =
-  let val consts = map (Sign.intern_const (Theory.sign_of thy)) raw_consts;
-  in PureThy.thms_containing thy consts end
-  handle THEORY (msg,_) => error msg;
+fun thms_containing_thy thy consts = PureThy.thms_containing thy consts
+  handle THEORY (msg, _) => error msg | THM (msg, _, _) => error msg;
+
+fun theory_of_goal () = ThyInfo.theory_of_sign (Thm.sign_of_thm (Goals.topthm ()));
+
+fun thms_containing raw_consts =
+  let
+    val thy = theory_of_goal ();
+    val consts = map (Sign.intern_const (Theory.sign_of thy)) raw_consts;
+  in thms_containing_thy thy consts end;
 
-fun thms_containing cs =
-  thms_containing_thy (ThyInfo.theory_of_sign (Thm.sign_of_thm (Goals.topthm ()))) cs;
+fun print_thms_containing thy ts =
+  let
+    val prt_const =
+      Pretty.quote o Pretty.str o Sign.cond_extern (Theory.sign_of thy) Sign.constK;
+    fun prt_thm (a, th) = Pretty.block [Pretty.str (a ^ ":"),
+      Pretty.brk 1, Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))];
 
-fun prt_thm (a, th) =
-  Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
-    Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))];
-
-fun print_thms_containing thy cs =
-  Pretty.writeln (Pretty.blk (0, Pretty.fbreaks (map prt_thm (thms_containing_thy thy cs))));
-
+    val cs = foldr Term.add_term_consts (ts, []);
+    val header =
+      if Library.null cs then []
+      else [Pretty.block (Pretty.breaks (Pretty.str "theorems containing constants:" ::
+          map prt_const cs)), Pretty.str ""];
+  in
+    if Library.null cs andalso not (Library.null ts) then
+      warning "thms_containing: no constants in specification"
+    else (header @ map prt_thm (thms_containing_thy thy cs)) |> Pretty.chunks |> Pretty.writeln
+  end;
 
 (*top_const: main constant, ignoring Trueprop*)
 fun top_const (_ $ t) = (case head_of t of Const (c, _) => Some c | _ => None)
@@ -133,13 +145,13 @@
 (* could be provided by thm db *)
 fun index_intros c =
   let fun topc(_,thm) = intro_const thm = Some(c);
-      val named_thms = thms_containing [c]
+      val named_thms = thms_containing_thy (theory_of_goal ()) [c]
   in filter topc named_thms end;
 
 (* could be provided by thm db *)
 fun index_elims c =
   let fun topc(_,thm) = elim_const thm = Some(c);
-      val named_thms = thms_containing [c]
+      val named_thms = thms_containing_thy (theory_of_goal ()) [c]
   in filter topc named_thms end;
 
 (*assume that parameters have unique names; reverse them for substitution*)