src/Pure/Isar/element.ML

     | a => Pretty.block [Pretty.command kind, Pretty.brk 1, Pretty.str (Sign.base_name a ^ ":")])
   in Pretty.block (Pretty.fbreaks (head :: prts)) end;
 
 fun obtain prop ctxt =
   let
-    val xs = ProofContext.rename_frees ctxt [] (Logic.strip_params prop);
+    val xs = Variable.rename_wrt ctxt [] (Logic.strip_params prop);
     val args = rev (map Free xs);
     val As = Logic.strip_assums_hyp prop |> map (fn t => Term.subst_bounds (args, t));
-    val ctxt' = ctxt |> fold ProofContext.declare_term args;
+    val ctxt' = ctxt |> fold Variable.declare_term args;
   in (("", (map (apsnd SOME) xs, As)), ctxt') end;
 
 in
 
 fun pretty_statement ctxt kind raw_th =

         val C' = Var ((AutoBind.thesisN, Thm.maxidx_of th + 1), Term.fastype_of C);
       in Term.subst_atomic [(C, C')] t end;
 
     val raw_prop =
       Thm.prop_of th
-      |> singleton (ProofContext.monomorphic ctxt)
+      |> singleton (Variable.monomorphic ctxt)
       |> K (ObjectLogic.is_elim th) ? standard_thesis
       |> Term.zero_var_indexes;
 
     val vars = Term.add_vars raw_prop [];
-    val frees = ProofContext.rename_frees ctxt [raw_prop] (map (apfst fst) vars);
+    val frees = Variable.rename_wrt ctxt [raw_prop] (map (apfst fst) vars);
     val fixes = rev (filter_out (fn (x, _) => x = AutoBind.thesisN) frees);
 
     val prop = Term.instantiate ([], vars ~~ map Free frees) raw_prop;
     val (prems, concl) = Logic.strip_horn prop;
     val thesis = ObjectLogic.fixed_judgment thy AutoBind.thesisN;

   in
     pretty_ctxt ctxt (Fixes (map (fn (x, T) => (x, SOME T, NoSyn)) fixes)) @
     pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, [])])) asms)) @
     pretty_stmt ctxt
      (if null cases then Shows [(("", []), [(concl, [])])]
-      else Obtains (#1 (fold_map obtain cases (ctxt |> ProofContext.declare_term prop))))
+      else Obtains (#1 (fold_map obtain cases (ctxt |> Variable.declare_term prop))))
   end |> thm_name kind raw_th;
 
 end;