1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Aug 26 11:33:36 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Aug 26 12:06:00 2010 +0200
     1.3 @@ -185,10 +185,9 @@
     1.4  
     1.5  fun compile_term compilation options ctxt t =
     1.6    let
     1.7 -    val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
     1.8 -    val thy = (ProofContext.theory_of ctxt') 
     1.9 +    val thy = Theory.copy (ProofContext.theory_of ctxt)
    1.10      val (vs, t') = strip_abs t
    1.11 -    val vs' = Variable.variant_frees ctxt' [] vs
    1.12 +    val vs' = Variable.variant_frees ctxt [] vs
    1.13      val t'' = subst_bounds (map Free (rev vs'), t')
    1.14      val (prems, concl) = strip_horn t''
    1.15      val constname = "pred_compile_quickcheck"