--- a/src/Pure/Thy/thm_database.ML Thu Oct 30 09:59:38 1997 +0100
+++ b/src/Pure/Thy/thm_database.ML Thu Oct 30 10:01:46 1997 +0100
@@ -63,17 +63,15 @@
-(** retrieve theorems **) (*peek at current proof state*)
+(** retrieve theorems **)
-(*get theorems that contain *all* of given constants*)
+(*get theorems that contain all of given constants*)
fun thms_containing raw_consts =
let
val sign = sign_of_thm (topthm ());
val consts = map (Sign.intern_const sign) raw_consts;
val thy = ThyInfo.theory_of_sign sign;
- in
- PureThy.thms_containing thy (consts \\ PureThy.ignored_consts)
- end;
+ in PureThy.thms_containing thy consts end;
(*top_const: main constant, ignoring Trueprop*)