src/HOL/Import/shuffler.ML
changeset 20224 9c40a144ee0e
parent 20071 8f3e1ddb50e6
child 20326 cbf31171c147
     1.1 --- a/src/HOL/Import/shuffler.ML	Thu Jul 27 13:43:00 2006 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Thu Jul 27 13:43:01 2006 +0200
     1.3 @@ -665,7 +665,7 @@
     1.4  fun search_meth ctxt =
     1.5      let
     1.6  	val thy = ProofContext.theory_of ctxt
     1.7 -	val prems = ProofContext.prems_of ctxt
     1.8 +	val prems = Assumption.prems_of ctxt
     1.9      in
    1.10  	Method.SIMPLE_METHOD' HEADGOAL (gen_shuffle_tac thy true (map (pair "premise") prems))
    1.11      end