src/HOL/Tools/Predicate_Compile/code_prolog.ML

       (Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq}))))
     (Thm.transfer thy rule)
 
 fun translate_intros ensure_groundness ctxt gr const constant_table =
   let
-    val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const)
+    val intros = map (preprocess_intro (Proof_Context.theory_of ctxt)) (Graph.get_node gr const)
     val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt
     val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table
     fun translate_intro intro =
       let
         val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro)

             ((rel_name, lim_var @ [maybe_AppF (translate_const constant_table'' constr_name, vars)]),
              Conj (map2 mk_prem vars Ts))
         in
           (clause :: flat rec_clauses, (seen', constant_table''))
         end
-      val constrs = inst_constrs_of (ProofContext.theory_of ctxt) T
+      val constrs = inst_constrs_of (Proof_Context.theory_of ctxt) T
       val constrs' = (constrs ~~ map (is_recursive_constr T) constrs)
         |> (fn cs => filter_out snd cs @ filter snd cs)
       val (clauses, constant_table') =
         apfst flat (fold_map mk_impl constrs' (T :: seen, constant_table))
       val size_term = funpow size (fn t => AppF ("suc", [t])) (Cons "zero")

   | restore_term ctxt constant_table (Number n, @{typ "int"}) = HOLogic.mk_number @{typ "int"} n
   | restore_term ctxt constant_table (Number n, _) = raise (Fail "unexpected type for number") 
   | restore_term ctxt constant_table (Cons s, T) = Const (restore_const constant_table s, T)
   | restore_term ctxt constant_table (AppF (f, args), T) =
     let
-      val thy = ProofContext.theory_of ctxt
+      val thy = Proof_Context.theory_of ctxt
       val c = restore_const constant_table f
       val cT = Sign.the_const_type thy c
       val (argsT, resT) = strip_type cT
       val subst = Sign.typ_match thy (resT, T) Vartab.empty
       val argsT' = map (Envir.subst_type subst) argsT

   compilation = Predicate_Compile_Aux.Pred
 }
 
 fun values ctxt soln t_compr =
   let
-    val options = code_options_of (ProofContext.theory_of ctxt)
+    val options = code_options_of (Proof_Context.theory_of ctxt)
     val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
       | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
     val (body, Ts, fp) = HOLogic.strip_psplits split;
     val output_names = Name.variant_list (Term.add_free_names body [])
       (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))

     val (pred as Const (name, T), all_args) =
       case strip_comb body of
         (Const (name, T), all_args) => (Const (name, T), all_args)
       | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)
     val _ = tracing "Preprocessing specification..."
-    val T = Sign.the_const_type (ProofContext.theory_of ctxt) name
+    val T = Sign.the_const_type (Proof_Context.theory_of ctxt) name
     val t = Const (name, T)
     val thy' =
-      Theory.copy (ProofContext.theory_of ctxt)
+      Theory.copy (Proof_Context.theory_of ctxt)
       |> Predicate_Compile.preprocess preprocess_options t
-    val ctxt' = ProofContext.init_global thy'
+    val ctxt' = Proof_Context.init_global thy'
     val _ = tracing "Generating prolog program..."
     val (p, constant_table) = generate (NONE, #ensure_groundness options) ctxt' name (* FIXME *)
       |> post_process ctxt' options name
     val constant_table' = declare_consts (fold Term.add_const_names all_args []) constant_table
     val args' = map (translate_term ctxt constant_table') all_args

 (* FIXME: a small clone of Predicate_Compile_Quickcheck - maybe refactor out commons *)
 
 fun quickcheck ctxt [(t, [])] [_, size] =
   let
     val t' = list_abs_free (Term.add_frees t [], t)
-    val options = code_options_of (ProofContext.theory_of ctxt)
-    val thy = Theory.copy (ProofContext.theory_of ctxt)
+    val options = code_options_of (Proof_Context.theory_of ctxt)
+    val thy = Theory.copy (Proof_Context.theory_of ctxt)
     val ((((full_constname, constT), vs'), intro), thy1) =
       Predicate_Compile_Aux.define_quickcheck_predicate t' thy
     val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
     val thy3 = Predicate_Compile.preprocess preprocess_options (Const (full_constname, constT)) thy2
-    val ctxt' = ProofContext.init_global thy3
+    val ctxt' = Proof_Context.init_global thy3
     val _ = tracing "Generating prolog program..."
     val (p, constant_table) = generate (NONE, true) ctxt' full_constname
       |> post_process ctxt' (set_ensure_groundness options) full_constname
     val _ = tracing "Running prolog program..."
     val system_config = System_Config.get (Context.Proof ctxt)