src/Pure/Isar/locale.ML

   val extend = I;
   val merge = Name_Space.join_tables (K merge_locale);
 );
 
 val intern = Name_Space.intern o #1 o Locales.get;
-fun extern thy = Name_Space.extern (ProofContext.init_global thy) (#1 (Locales.get thy));
+fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (#1 (Locales.get thy));
 
 val get_locale = Symtab.lookup o #2 o Locales.get;
 val defined = Symtab.defined o #2 o Locales.get;
 
 fun the_locale thy name =

 
 (* Print instance and qualifiers *)
 
 fun pretty_reg ctxt (name, morph) =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     val name' = extern thy name;
     fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
     fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     fun prt_term' t =

     |-> put_idents
   end;
 
 fun init name thy =
   activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
-    ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
+    ([], Context.Proof (Proof_Context.init_global thy)) |-> put_idents |> Context.proof_of;
 
 
 (*** Add and extend registrations ***)
 
 fun amend_registration (name, morph) mixin export context =

 (* Theorems *)
 
 fun add_thmss loc kind args ctxt =
   let
     val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
-    val ctxt'' = ctxt' |> ProofContext.background_theory
+    val ctxt'' = ctxt' |> Proof_Context.background_theory
      ((change_locale loc o apfst o apsnd) (cons (args', serial ()))
         #>
       (* Registrations *)
       (fn thy => fold_rev (fn (_, morph) =>
             let

     [((Binding.conceal Binding.empty,
         [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
       [([Drule.dummy_thm], [])])];
 
 fun add_syntax_declaration loc decl =
-  ProofContext.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
+  Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
   #> add_declaration loc decl;
 
 
 (*** Reasoning about locales ***)
 

 
 val all_locales = Symtab.keys o snd o Locales.get;
 
 fun print_locales thy =
   Pretty.strs ("locales:" ::
-    map #1 (Name_Space.extern_table (ProofContext.init_global thy) (Locales.get thy)))
+    map #1 (Name_Space.extern_table (Proof_Context.init_global thy) (Locales.get thy)))
   |> Pretty.writeln;
 
 fun print_locale thy show_facts raw_name =
   let
     val name = intern thy raw_name;

     |> Pretty.writeln
   end;
 
 fun print_registrations ctxt raw_name =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     val name = intern thy raw_name;
     val _ = the_locale thy name;  (* error if locale unknown *)
   in
     (case registrations_of (Context.Proof ctxt) (* FIXME *) name of
       [] => Pretty.str ("no interpretations")
     | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt) (rev regs)))
   end |> Pretty.writeln;
 
 fun print_dependencies ctxt clean export insts =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     val idents = if clean then [] else get_idents (Context.Proof ctxt);
   in
     (case fold (roundup thy cons export) insts (idents, []) |> snd of
       [] => Pretty.str ("no dependencies")
     | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps)))