src/Pure/goal.ML
changeset 30473 e0b66c11e7e4
parent 29448 34b9652b2f45
child 32056 f4b74cbecdaf
     1.1 --- a/src/Pure/goal.ML	Thu Mar 12 15:54:19 2009 +0100
     1.2 +++ b/src/Pure/goal.ML	Thu Mar 12 15:54:58 2009 +0100
     1.3 @@ -110,7 +110,7 @@
     1.4      val cert = Thm.cterm_of thy;
     1.5      val certT = Thm.ctyp_of thy;
     1.6  
     1.7 -    val assms = Assumption.assms_of ctxt;
     1.8 +    val assms = Assumption.all_assms_of ctxt;
     1.9      val As = map Thm.term_of assms;
    1.10  
    1.11      val xs = map Free (fold Term.add_frees (prop :: As) []);