src/HOL/Import/shuffler.ML
changeset 17892 62c397c17d18
parent 17463 e9c1574d0caf
child 17959 8db36a108213
     1.1 --- a/src/HOL/Import/shuffler.ML	Tue Oct 18 17:59:24 2005 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Tue Oct 18 17:59:25 2005 +0200
     1.3 @@ -490,8 +490,9 @@
     1.4  	val sg = sign_of thy
     1.5  
     1.6  	val norms = ShuffleData.get thy
     1.7 -	val ss = empty_ss setmksimps single
     1.8 -			  addsimps (map (Thm.transfer sg) norms)
     1.9 +	val ss = Simplifier.theory_context thy empty_ss
    1.10 +          setmksimps single
    1.11 +	  addsimps (map (Thm.transfer sg) norms)
    1.12  	fun chain f th =
    1.13  	    let
    1.14                  val rhs = snd (dest_equals (cprop_of th))