src/Pure/Tools/find_theorems.ML
changeset 30473 e0b66c11e7e4
parent 30364 577edc39b501
child 30693 c672c8162f4b
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Mar 12 15:54:19 2009 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Mar 12 15:54:58 2009 +0100
     1.3 @@ -336,7 +336,7 @@
     1.4  
     1.5  fun find_theorems ctxt opt_goal rem_dups raw_criteria =
     1.6    let
     1.7 -    val add_prems = Seq.hd o (TRY (Method.insert_tac (Assumption.prems_of ctxt) 1));
     1.8 +    val add_prems = Seq.hd o (TRY (Method.insert_tac (Assumption.all_prems_of ctxt) 1));
     1.9      val opt_goal' = Option.map add_prems opt_goal;
    1.10  
    1.11      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;