src/Pure/Isar/obtain.ML

         space_implode " " (map (Syntax.string_of_term ctxt) bads));
   in tm end;
 
 fun eliminate fix_ctxt rule xs As thm =
   let
-    val thy = ProofContext.theory_of fix_ctxt;
+    val thy = Proof_Context.theory_of fix_ctxt;
 
     val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
     val _ = Object_Logic.is_judgment thy (Thm.concl_of thm) orelse
       error "Conclusion in obtained context must be object-logic judgment";
 

 
 (** obtain **)
 
 fun bind_judgment ctxt name =
   let
-    val (bind, ctxt') = ProofContext.bind_fixes [name] ctxt;
-    val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (ProofContext.theory_of ctxt) name);
+    val (bind, ctxt') = Proof_Context.bind_fixes [name] ctxt;
+    val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (Proof_Context.theory_of ctxt) name);
   in ((v, t), ctxt') end;
 
 val thatN = "that";
 
 local

     val ctxt = Proof.context_of state;
     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
     (*obtain vars*)
     val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
-    val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
+    val (_, fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
     val xs = map (Variable.name o #1) vars;
 
     (*obtain asms*)
     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
     val asm_props = maps (map fst) proppss;

     val thesisN = Name.variant xs Auto_Bind.thesisN;
     val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN);
 
     val asm_frees = fold Term.add_frees asm_props [];
     val parms = xs |> map (fn x =>
-      let val x' = ProofContext.get_skolem fix_ctxt x
+      let val x' = Proof_Context.get_skolem fix_ctxt x
       in (x', the_default propT (AList.lookup (op =) asm_frees x')) end);
 
     val that_name = if name = "" then thatN else name;
     val that_prop =
       Term.list_all_free (parms, Logic.list_implies (asm_props, thesis))

     |-> Proof.refine_insert
   end;
 
 in
 
-val obtain = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
-val obtain_cmd = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
+val obtain = gen_obtain (K I) Proof_Context.cert_vars Proof_Context.cert_propp;
+val obtain_cmd = gen_obtain Attrib.attribute Proof_Context.read_vars Proof_Context.read_propp;
 
 end;
 
 
 

   | [] => error "Goal solved -- nothing guessed"
   | _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
 
 fun result tac facts ctxt =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
     val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN;
     val rule =
       (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of

 
 local
 
 fun unify_params vars thesis_var raw_rule ctxt =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     val certT = Thm.ctyp_of thy;
     val cert = Thm.cterm_of thy;
     val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
 
     fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);

   in ((vars', rule''), ctxt') end;
 
 fun inferred_type (binding, _, mx) ctxt =
   let
     val x = Variable.name binding;
-    val (T, ctxt') = ProofContext.inferred_param x ctxt
+    val (T, ctxt') = Proof_Context.inferred_param x ctxt
   in ((x, T, mx), ctxt') end;
 
 fun polymorphic ctxt vars =
   let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars))
   in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end;

 
     fun guess_context raw_rule state' =
       let
         val ((parms, rule), ctxt') =
           unify_params vars thesis_var raw_rule (Proof.context_of state');
-        val (bind, _) = ProofContext.bind_fixes (map (#1 o #1) parms) ctxt';
+        val (bind, _) = Proof_Context.bind_fixes (map (#1 o #1) parms) ctxt';
         val ts = map (bind o Free o #1) parms;
         val ps = map dest_Free ts;
         val asms =
           Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
           |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), []));

     |> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
   end;
 
 in
 
-val guess = gen_guess ProofContext.cert_vars;
-val guess_cmd = gen_guess ProofContext.read_vars;
+val guess = gen_guess Proof_Context.cert_vars;
+val guess_cmd = gen_guess Proof_Context.read_vars;
 
 end;
 
 end;