src/Pure/Isar/obtain.ML

     (*obtain asms*)
     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
     val asm_props = maps (map fst) proppss;
     val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
 
-    val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
+    val _ = Variable.warn_extra_tfrees fix_ctxt asms_ctxt;
 
     (*obtain statements*)
     val thesisN = Term.variant xs AutoBind.thesisN;
     val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN;
 

 fun inferred_type (x, _, mx) ctxt =
   let val ((_, T), ctxt') = ProofContext.inferred_param x ctxt
   in ((x, T, mx), ctxt') end;
 
 fun polymorphic (vars, ctxt) =
-  let val Ts = map Logic.dest_type (ProofContext.polymorphic ctxt (map (Logic.mk_type o #2) 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 gen_guess prep_vars raw_vars int state =
   let
     val _ = Proof.assert_forward_or_chain state;

           let
             val xs = map fst vars;
             val props = map fst propp;
             val (parms, ctxt'') =
               ctxt'
-              |> fold ProofContext.declare_term props
+              |> fold Variable.declare_term props
               |> fold_map ProofContext.inferred_param xs;
             val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
           in
             ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
             ctxt' |> ProofContext.add_assms_i ProofContext.assume_export