src/Pure/Isar/proof.ML

   val assert_bottom: bool -> state -> state
   val context_of: state -> context
   val theory_of: state -> theory
   val sign_of: state -> theory    (*obsolete*)
   val map_context: (context -> context) -> state -> state
-  val warn_extra_tfrees: state -> state -> state
   val add_binds_i: (indexname * term option) list -> state -> state
   val put_thms: bool -> string * thm list option -> state -> state
   val put_thms_internal: string * thm list option -> state -> state
   val the_facts: state -> thm list
   val the_fact: state -> thm

   map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
 
 fun map_context_result f state =
   f (context_of state) ||> (fn ctxt => map_context (K ctxt) state);
 
-val warn_extra_tfrees = map_context o ProofContext.warn_extra_tfrees o context_of;
 val add_binds_i = map_context o ProofContext.add_binds_i;
 val put_thms = map_context oo ProofContext.put_thms;
 val put_thms_internal = map_context o ProofContext.put_thms_internal;
 
 

     val goal = Goal.init (Thm.cterm_of thy (Logic.mk_conjunction_list2 propss'));
     val after_qed' = after_qed |>> (fn after_local =>
       fn results => map_context after_ctxt #> after_local results);
   in
     goal_state
-    |> map_context (ProofContext.set_body true)
+    |> map_context (Variable.set_body true)
     |> put_goal (SOME (make_goal ((kind, propss'), [], goal, before_qed, after_qed')))
     |> map_context (ProofContext.add_cases false (AutoBind.cases thy props))
     |> map_context (ProofContext.auto_bind_goal props)
     |> K chaining ? (`the_facts #-> using_facts)
     |> put_facts NONE

     val outer_state = state |> close_block;
     val outer_ctxt = context_of outer_state;
 
     val props =
       flat (tl stmt)
-      |> ProofContext.generalize goal_ctxt outer_ctxt;
+      |> Variable.generalize goal_ctxt outer_ctxt;
     val results =
       tl (conclude_goal state goal stmt)
       |> (Seq.map_list o Seq.map_list) (ProofContext.exports goal_ctxt outer_ctxt);
   in
     outer_state

       #-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
       #> after_qed results;
   in
     state
     |> generic_goal prepp (kind ^ goal_names NONE "" names) before_qed (after_qed', K I) propp
-    |> warn_extra_tfrees state
+    |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
   end;
 
 fun local_qed txt =
   end_proof false txt
   #> Seq.map generic_qed