Use assms rather than prems in find_theorems solves.
authorTimothy Bourke
Tue, 24 Mar 2009 15:55:11 +1100
changeset 30693 c672c8162f4b
parent 30692 44ea10bc07a7
child 30695 182fb8d27b48
Use assms rather than prems in find_theorems solves.
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;