--- a/src/Pure/Tools/find_theorems.ML Mon Mar 23 14:29:59 2009 -0700
+++ b/src/Pure/Tools/find_theorems.ML Tue Mar 24 15:55:11 2009 +1100
@@ -336,7 +336,9 @@
fun find_theorems ctxt opt_goal rem_dups raw_criteria =
let
- val add_prems = Seq.hd o (TRY (Method.insert_tac (Assumption.all_prems_of ctxt) 1));
+ val assms = ProofContext.get_fact ctxt (Facts.named "local.assms")
+ handle ERROR _ => [];
+ val add_prems = Seq.hd o (TRY (Method.insert_tac assms 1));
val opt_goal' = Option.map add_prems opt_goal;
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;