src/Pure/Isar/rule_insts.ML

   let
     fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
     val ts = map2 parse Ts ss;
     val ts' =
       map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
-      |> Syntax.check_terms ((schematic ? ProofContext.set_mode ProofContext.mode_schematic) ctxt)
+      |> Syntax.check_terms ((schematic ? Proof_Context.set_mode Proof_Context.mode_schematic) ctxt)
       |> Variable.polymorphic ctxt;
     val Ts' = map Term.fastype_of ts';
     val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
   in (ts', map (apsnd snd) (Vartab.dest tyenv)) end;
 
 fun read_insts ctxt mixed_insts (tvars, vars) =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     val cert = Thm.cterm_of thy;
     val certT = Thm.ctyp_of thy;
 
     val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts;
     val internal_insts = term_insts |> map_filter

 
 
 (* instantiation of rule or goal state *)
 
 fun read_instantiate ctxt args thm =
-  read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic)  (* FIXME !? *)
+  read_instantiate_mixed (ctxt |> Proof_Context.set_mode Proof_Context.mode_schematic)  (* FIXME !? *)
     (map (fn (x, y) => (Token.eof, (x, Token.Text y))) args) thm;
 
 fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
 
 

 
 (* FIXME cleanup this mess!!! *)
 
 fun bires_inst_tac bires_flag ctxt insts thm =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     (* Separate type and term insts *)
     fun has_type_var ((x, _), _) =
       (case Symbol.explode x of "'" :: _ => true | _ => false);
     val Tinsts = filter has_type_var insts;
     val tinsts = filter_out has_type_var insts;

           (*the same name are renamed during printing*)
 
         val (param_names, ctxt') = ctxt
           |> Variable.declare_thm thm
           |> Thm.fold_terms Variable.declare_constraints st
-          |> ProofContext.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
+          |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
 
         (* Process type insts: Tinsts_env *)
         fun absent xi = error
               ("No such variable in theorem: " ^ Term.string_of_vname xi);
         val (rtypes, rsorts) = Drule.types_sorts thm;