# HG changeset patch
# User Timothy Bourke
# Date 1237870511 -39600
# Node ID c672c8162f4b59c146fa4af5ede72edba141dfa9
# Parent  44ea10bc07a73a4ed8357ada26c13a3c5dba468c
Use assms rather than prems in find_theorems solves.

diff -r 44ea10bc07a7 -r c672c8162f4b src/Pure/Tools/find_theorems.ML
--- 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;