# HG changeset patch
# User wenzelm
# Date 1282817160 -7200
# Node ID a37d39fe32f8d8310a6efde92aea0313122d91c3
# Parent  0ab848f84accc02e553f074e2714c19b489c0755
standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;

diff -r 0ab848f84acc -r a37d39fe32f8 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 26 11:33:36 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 26 12:06:00 2010 +0200
@@ -530,12 +530,13 @@
     val _ = tracing "Preprocessing specification..."
     val T = Sign.the_const_type (ProofContext.theory_of ctxt) name
     val t = Const (name, T)
-    val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
-    val thy' = Predicate_Compile.preprocess preprocess_options t (ProofContext.theory_of ctxt')
-    val ctxt'' = ProofContext.init_global thy'
+    val thy' =
+      Theory.copy (ProofContext.theory_of ctxt)
+      |> Predicate_Compile.preprocess preprocess_options t
+    val ctxt' = ProofContext.init_global thy'
     val _ = tracing "Generating prolog program..."
-    val (p, constant_table) = generate options ctxt'' name
-      |> (if #ensure_groundness options then add_ground_predicates ctxt'' else I)
+    val (p, constant_table) = generate options ctxt' name
+      |> (if #ensure_groundness options then add_ground_predicates ctxt' else I)
     val _ = tracing "Running prolog program..."
     val tss = run p (translate_const constant_table name) (map first_upper vnames) soln
     val _ = tracing "Restoring terms..."
@@ -553,7 +554,7 @@
             mk_set_compr (t :: in_insert) ts xs
           else
             let
-              val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt'' [t]) ("uu", fastype_of t)
+              val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt' [t]) ("uu", fastype_of t)
               val set_compr =
                 HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
                   frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"})))
@@ -564,7 +565,7 @@
         end
   in
       foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr []
-        (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt'' constant_table) (ts ~~ Ts))) tss) [])
+        (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt' constant_table) (ts ~~ Ts))) tss) [])
   end
 
 fun values_cmd print_modes soln raw_t state =
@@ -605,10 +606,9 @@
 
 fun quickcheck ctxt report t size =
   let
-    val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
-    val thy = (ProofContext.theory_of ctxt')
+    val thy = Theory.copy (ProofContext.theory_of ctxt)
     val (vs, t') = strip_abs t
-    val vs' = Variable.variant_frees ctxt' [] vs
+    val vs' = Variable.variant_frees ctxt [] vs
     val Ts = map snd vs'
     val t'' = subst_bounds (map Free (rev vs'), t')
     val (prems, concl) = strip_horn t''
@@ -624,15 +624,15 @@
     val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
     val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
     val thy3 = Predicate_Compile.preprocess preprocess_options const thy2
-    val ctxt'' = ProofContext.init_global thy3
+    val ctxt' = ProofContext.init_global thy3
     val _ = tracing "Generating prolog program..."
-    val (p, constant_table) = generate {ensure_groundness = true} ctxt'' full_constname
-      |> add_ground_predicates ctxt''
+    val (p, constant_table) = generate {ensure_groundness = true} ctxt' full_constname
+      |> add_ground_predicates ctxt'
     val _ = tracing "Running prolog program..."
     val [ts] = run p (translate_const constant_table full_constname) (map fst vs')
       (SOME 1)
     val _ = tracing "Restoring terms..."
-    val res = SOME (map (restore_term ctxt'' constant_table) (ts ~~ Ts))
+    val res = SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
     val empty_report = ([], false)
   in
     (res, empty_report)
diff -r 0ab848f84acc -r a37d39fe32f8 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Aug 26 11:33:36 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Aug 26 12:06:00 2010 +0200
@@ -185,10 +185,9 @@
 
 fun compile_term compilation options ctxt t =
   let
-    val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
-    val thy = (ProofContext.theory_of ctxt') 
+    val thy = Theory.copy (ProofContext.theory_of ctxt)
     val (vs, t') = strip_abs t
-    val vs' = Variable.variant_frees ctxt' [] vs
+    val vs' = Variable.variant_frees ctxt [] vs
     val t'' = subst_bounds (map Free (rev vs'), t')
     val (prems, concl) = strip_horn t''
     val constname = "pred_compile_quickcheck"