ProofContext: moved variable operations to struct Variable;
tuned;

--- a/src/Pure/Isar/locale.ML	Thu Jun 15 23:08:58 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Jun 15 23:10:45 2006 +0200
@@ -513,11 +513,8 @@
 (* parameter types *)
 
 fun frozen_tvars ctxt Ts =
-  let
-    val tvars = rev (fold Term.add_tvarsT Ts []);
-    val tfrees = map TFree
-      (Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars);
-  in map (fn ((xi, S), T) => (xi, (S, T))) (tvars ~~ tfrees) end;
+  #1 (Variable.monomorphic_inst (map Logic.mk_type Ts) ctxt)
+  |> map (fn ((xi, S), T) => (xi, (S, T)));
 
 fun unify_frozen ctxt maxidx Ts Us =
   let
@@ -1058,7 +1055,7 @@
        Parameters new in context elements must receive types that are
        distinct from types of parameters in target (fixed_params).  *)
     val ctxt_with_fixed =
-      fold ProofContext.declare_term (map Free fixed_params) ctxt;
+      fold Variable.declare_term (map Free fixed_params) ctxt;
     val int_elemss =
       raw_elemss
       |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
@@ -1141,8 +1138,7 @@
   | closeup ctxt true elem =
       let
         fun close_frees t =
-          let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1)
-            (Term.add_frees t []))
+          let val frees = rev (filter_out (Variable.is_fixed ctxt o #1) (Term.add_frees t []))
           in Term.list_all_free (frees, t) end;
 
         fun no_binds [] = []
@@ -1226,9 +1222,9 @@
         (* CB: add type information from fixed_params to context (declare_term) *)
         (* CB: process patterns (conclusion and external elements only) *)
         val (ctxt, all_propp) =
-          prepp (fold ProofContext.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
+          prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
         (* CB: add type information from conclusion and external elements to context *)
-        val ctxt = fold ProofContext.declare_term (maps (map fst) all_propp) ctxt;
+        val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
         (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
         val all_propp' = map2 (curry (op ~~))
           (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
@@ -1241,8 +1237,8 @@
     (* CB: obtain all parameters from identifier part of raw_elemss *)
     val xs = map #1 (params_of' raw_elemss);
     val typing = unify_frozen ctxt 0
-      (map (ProofContext.default_type raw_ctxt) xs)
-      (map (ProofContext.default_type ctxt) xs);
+      (map (Variable.default_type raw_ctxt) xs)
+      (map (Variable.default_type ctxt) xs);
     val parms = param_types (xs ~~ typing);
     (* CB: parms are the parameters from raw_elemss, with correct typing. *)
 

--- a/src/Pure/Isar/proof.ML	Thu Jun 15 23:08:58 2006 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Jun 15 23:10:45 2006 +0200
@@ -18,7 +18,6 @@
   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
@@ -202,7 +201,6 @@
 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;
@@ -807,7 +805,7 @@
       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)
@@ -829,7 +827,7 @@
 
     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);
@@ -855,7 +853,7 @@
   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 =