1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 26 11:33:36 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 26 12:06:00 2010 +0200
     1.3 @@ -530,12 +530,13 @@
     1.4      val _ = tracing "Preprocessing specification..."
     1.5      val T = Sign.the_const_type (ProofContext.theory_of ctxt) name
     1.6      val t = Const (name, T)
     1.7 -    val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
     1.8 -    val thy' = Predicate_Compile.preprocess preprocess_options t (ProofContext.theory_of ctxt')
     1.9 -    val ctxt'' = ProofContext.init_global thy'
    1.10 +    val thy' =
    1.11 +      Theory.copy (ProofContext.theory_of ctxt)
    1.12 +      |> Predicate_Compile.preprocess preprocess_options t
    1.13 +    val ctxt' = ProofContext.init_global thy'
    1.14      val _ = tracing "Generating prolog program..."
    1.15 -    val (p, constant_table) = generate options ctxt'' name
    1.16 -      |> (if #ensure_groundness options then add_ground_predicates ctxt'' else I)
    1.17 +    val (p, constant_table) = generate options ctxt' name
    1.18 +      |> (if #ensure_groundness options then add_ground_predicates ctxt' else I)
    1.19      val _ = tracing "Running prolog program..."
    1.20      val tss = run p (translate_const constant_table name) (map first_upper vnames) soln
    1.21      val _ = tracing "Restoring terms..."
    1.22 @@ -553,7 +554,7 @@
    1.23              mk_set_compr (t :: in_insert) ts xs
    1.24            else
    1.25              let
    1.26 -              val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt'' [t]) ("uu", fastype_of t)
    1.27 +              val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt' [t]) ("uu", fastype_of t)
    1.28                val set_compr =
    1.29                  HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
    1.30                    frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"})))
    1.31 @@ -564,7 +565,7 @@
    1.32          end
    1.33    in
    1.34        foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr []
    1.35 -        (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt'' constant_table) (ts ~~ Ts))) tss) [])
    1.36 +        (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt' constant_table) (ts ~~ Ts))) tss) [])
    1.37    end
    1.38  
    1.39  fun values_cmd print_modes soln raw_t state =
    1.40 @@ -605,10 +606,9 @@
    1.41  
    1.42  fun quickcheck ctxt report t size =
    1.43    let
    1.44 -    val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
    1.45 -    val thy = (ProofContext.theory_of ctxt')
    1.46 +    val thy = Theory.copy (ProofContext.theory_of ctxt)
    1.47      val (vs, t') = strip_abs t
    1.48 -    val vs' = Variable.variant_frees ctxt' [] vs
    1.49 +    val vs' = Variable.variant_frees ctxt [] vs
    1.50      val Ts = map snd vs'
    1.51      val t'' = subst_bounds (map Free (rev vs'), t')
    1.52      val (prems, concl) = strip_horn t''
    1.53 @@ -624,15 +624,15 @@
    1.54      val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
    1.55      val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
    1.56      val thy3 = Predicate_Compile.preprocess preprocess_options const thy2
    1.57 -    val ctxt'' = ProofContext.init_global thy3
    1.58 +    val ctxt' = ProofContext.init_global thy3
    1.59      val _ = tracing "Generating prolog program..."
    1.60 -    val (p, constant_table) = generate {ensure_groundness = true} ctxt'' full_constname
    1.61 -      |> add_ground_predicates ctxt''
    1.62 +    val (p, constant_table) = generate {ensure_groundness = true} ctxt' full_constname
    1.63 +      |> add_ground_predicates ctxt'
    1.64      val _ = tracing "Running prolog program..."
    1.65      val [ts] = run p (translate_const constant_table full_constname) (map fst vs')
    1.66        (SOME 1)
    1.67      val _ = tracing "Restoring terms..."
    1.68 -    val res = SOME (map (restore_term ctxt'' constant_table) (ts ~~ Ts))
    1.69 +    val res = SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
    1.70      val empty_report = ([], false)
    1.71    in
    1.72      (res, empty_report)

     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Aug 26 11:33:36 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Aug 26 12:06:00 2010 +0200
     2.3 @@ -185,10 +185,9 @@
     2.4  
     2.5  fun compile_term compilation options ctxt t =
     2.6    let
     2.7 -    val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
     2.8 -    val thy = (ProofContext.theory_of ctxt') 
     2.9 +    val thy = Theory.copy (ProofContext.theory_of ctxt)
    2.10      val (vs, t') = strip_abs t
    2.11 -    val vs' = Variable.variant_frees ctxt' [] vs
    2.12 +    val vs' = Variable.variant_frees ctxt [] vs
    2.13      val t'' = subst_bounds (map Free (rev vs'), t')
    2.14      val (prems, concl) = strip_horn t''
    2.15      val constname = "pred_compile_quickcheck"