ProofContext: moved variable operations to struct Variable;
authorwenzelm
Thu Jun 15 23:08:54 2006 +0200 (2006-06-15)
changeset 19897fe661eb3b0e7
parent 19896 286d950883bc
child 19898 b1d179e42713
ProofContext: moved variable operations to struct Variable;
src/Provers/project_rule.ML
src/Pure/Isar/element.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof_context.ML
src/Pure/Tools/codegen_theorems.ML
src/Pure/Tools/invoke.ML
     1.1 --- a/src/Provers/project_rule.ML	Thu Jun 15 18:35:16 2006 +0200
     1.2 +++ b/src/Provers/project_rule.ML	Thu Jun 15 23:08:54 2006 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4        (case try imp th of
     1.5          NONE => (k, th)
     1.6        | SOME th' => prems (k + 1) th');
     1.7 -    val ([rule], ctxt') = ProofContext.import true [raw_rule] ctxt;
     1.8 +    val ([rule], ctxt') = Variable.import true [raw_rule] ctxt;
     1.9      fun result i =
    1.10        rule
    1.11        |> proj i
    1.12 @@ -57,7 +57,7 @@
    1.13        (case try conj2 th of
    1.14          NONE => k
    1.15        | SOME th' => projs (k + 1) th');
    1.16 -    val ([rule], _) = ProofContext.import true [raw_rule] ctxt;
    1.17 +    val ([rule], _) = Variable.import true [raw_rule] ctxt;
    1.18    in projects ctxt (1 upto projs 1 rule) raw_rule end;
    1.19  
    1.20  end;
     2.1 --- a/src/Pure/Isar/element.ML	Thu Jun 15 18:35:16 2006 +0200
     2.2 +++ b/src/Pure/Isar/element.ML	Thu Jun 15 23:08:54 2006 +0200
     2.3 @@ -214,10 +214,10 @@
     2.4  
     2.5  fun obtain prop ctxt =
     2.6    let
     2.7 -    val xs = ProofContext.rename_frees ctxt [] (Logic.strip_params prop);
     2.8 +    val xs = Variable.rename_wrt ctxt [] (Logic.strip_params prop);
     2.9      val args = rev (map Free xs);
    2.10      val As = Logic.strip_assums_hyp prop |> map (fn t => Term.subst_bounds (args, t));
    2.11 -    val ctxt' = ctxt |> fold ProofContext.declare_term args;
    2.12 +    val ctxt' = ctxt |> fold Variable.declare_term args;
    2.13    in (("", (map (apsnd SOME) xs, As)), ctxt') end;
    2.14  
    2.15  in
    2.16 @@ -235,12 +235,12 @@
    2.17  
    2.18      val raw_prop =
    2.19        Thm.prop_of th
    2.20 -      |> singleton (ProofContext.monomorphic ctxt)
    2.21 +      |> singleton (Variable.monomorphic ctxt)
    2.22        |> K (ObjectLogic.is_elim th) ? standard_thesis
    2.23        |> Term.zero_var_indexes;
    2.24  
    2.25      val vars = Term.add_vars raw_prop [];
    2.26 -    val frees = ProofContext.rename_frees ctxt [raw_prop] (map (apfst fst) vars);
    2.27 +    val frees = Variable.rename_wrt ctxt [raw_prop] (map (apfst fst) vars);
    2.28      val fixes = rev (filter_out (fn (x, _) => x = AutoBind.thesisN) frees);
    2.29  
    2.30      val prop = Term.instantiate ([], vars ~~ map Free frees) raw_prop;
    2.31 @@ -252,7 +252,7 @@
    2.32      pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, [])])) asms)) @
    2.33      pretty_stmt ctxt
    2.34       (if null cases then Shows [(("", []), [(concl, [])])]
    2.35 -      else Obtains (#1 (fold_map obtain cases (ctxt |> ProofContext.declare_term prop))))
    2.36 +      else Obtains (#1 (fold_map obtain cases (ctxt |> Variable.declare_term prop))))
    2.37    end |> thm_name kind raw_th;
    2.38  
    2.39  end;
     3.1 --- a/src/Pure/Isar/local_defs.ML	Thu Jun 15 18:35:16 2006 +0200
     3.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Jun 15 23:08:54 2006 +0200
     3.3 @@ -40,7 +40,7 @@
     3.4      fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^ display_term eq);
     3.5      val ((lhs, _), eq') = eq
     3.6        |> Sign.no_vars pp
     3.7 -      |> Logic.dest_def pp Term.is_Free (ProofContext.is_fixed ctxt) (K true)
     3.8 +      |> Logic.dest_def pp Term.is_Free (Variable.is_fixed ctxt) (K true)
     3.9        handle TERM (msg, _) => err msg | ERROR msg => err msg;
    3.10    in (Term.dest_Free (Term.head_of lhs), eq') end;
    3.11  
    3.12 @@ -157,7 +157,7 @@
    3.13          val thy' = ProofContext.theory_of ctxt';
    3.14          val prop' = Term.subst_atomic [(Free (c, T), t)] prop;
    3.15          val frees = Term.fold_aterms (fn Free (x, _) =>
    3.16 -          if ProofContext.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
    3.17 +          if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
    3.18        in
    3.19          Goal.prove thy' frees [] prop' (K (ALLGOALS
    3.20            (meta_rewrite_tac ctxt' THEN'
     4.1 --- a/src/Pure/Isar/obtain.ML	Thu Jun 15 18:35:16 2006 +0200
     4.2 +++ b/src/Pure/Isar/obtain.ML	Thu Jun 15 23:08:54 2006 +0200
     4.3 @@ -121,7 +121,7 @@
     4.4      val asm_props = maps (map fst) proppss;
     4.5      val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
     4.6  
     4.7 -    val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
     4.8 +    val _ = Variable.warn_extra_tfrees fix_ctxt asms_ctxt;
     4.9  
    4.10      (*obtain statements*)
    4.11      val thesisN = Term.variant xs AutoBind.thesisN;
    4.12 @@ -220,7 +220,7 @@
    4.13    in ((x, T, mx), ctxt') end;
    4.14  
    4.15  fun polymorphic (vars, ctxt) =
    4.16 -  let val Ts = map Logic.dest_type (ProofContext.polymorphic ctxt (map (Logic.mk_type o #2) vars))
    4.17 +  let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars))
    4.18    in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end;
    4.19  
    4.20  fun gen_guess prep_vars raw_vars int state =
    4.21 @@ -308,7 +308,7 @@
    4.22              val props = map fst propp;
    4.23              val (parms, ctxt'') =
    4.24                ctxt'
    4.25 -              |> fold ProofContext.declare_term props
    4.26 +              |> fold Variable.declare_term props
    4.27                |> fold_map ProofContext.inferred_param xs;
    4.28              val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
    4.29            in
     5.1 --- a/src/Pure/Isar/proof_context.ML	Thu Jun 15 18:35:16 2006 +0200
     5.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Jun 15 23:08:54 2006 +0200
     5.3 @@ -4,7 +4,7 @@
     5.4  
     5.5  The key concept of Isar proof contexts: elevates primitive local
     5.6  reasoning Gamma |- phi to a structured concept, with generic context
     5.7 -elements, polymorphic abbreviations, and extra-logical data.
     5.8 +elements.
     5.9  *)
    5.10  
    5.11  signature PROOF_CONTEXT =
    5.12 @@ -15,15 +15,11 @@
    5.13    val init: theory -> context
    5.14    val full_name: context -> bstring -> string
    5.15    val consts_of: context -> Consts.T
    5.16 -  val set_body: bool -> context -> context
    5.17 -  val restore_body: context -> context -> context
    5.18    val set_syntax_mode: string * bool -> context -> context
    5.19    val restore_syntax_mode: context -> context -> context
    5.20    val assms_of: context -> term list
    5.21    val prems_of: context -> thm list
    5.22    val fact_index_of: context -> FactIndex.T
    5.23 -  val is_fixed: context -> string -> bool
    5.24 -  val is_known: context -> string -> bool
    5.25    val transfer: theory -> context -> context
    5.26    val map_theory: (theory -> theory) -> context -> context
    5.27    val pretty_term: context -> term -> Pretty.T
    5.28 @@ -40,9 +36,6 @@
    5.29    val string_of_typ: context -> typ -> string
    5.30    val string_of_term: context -> term -> string
    5.31    val string_of_thm: context -> thm -> string
    5.32 -  val used_types: context -> string list
    5.33 -
    5.34 -  val default_type: context -> string -> typ option
    5.35    val read_typ: context -> string -> typ
    5.36    val read_typ_syntax: context -> string -> typ
    5.37    val read_typ_abbrev: context -> string -> typ
    5.38 @@ -68,25 +61,15 @@
    5.39    val cert_prop: context -> term -> term
    5.40    val cert_term_pats: typ -> context -> term list -> term list
    5.41    val cert_prop_pats: context -> term list -> term list
    5.42 -  val declare_type: typ -> context -> context
    5.43 -  val declare_term: term -> context -> context
    5.44 -  val invent_types: sort list -> context -> (string * sort) list * context
    5.45    val infer_type: context -> string -> typ
    5.46    val inferred_param: string -> context -> (string * typ) * context
    5.47    val inferred_fixes: context -> (string * typ) list * context
    5.48    val read_tyname: context -> string -> typ
    5.49    val read_const: context -> string -> term
    5.50 -  val rename_frees: context -> term list -> (string * 'a) list -> (string * 'a) list
    5.51 -  val warn_extra_tfrees: context -> context -> context
    5.52 -  val generalize: context -> context -> term list -> term list
    5.53 -  val monomorphic: context -> term list -> term list
    5.54 -  val polymorphic: context -> term list -> term list
    5.55 -  val hidden_polymorphism: term -> typ -> (indexname * sort) list
    5.56    val goal_exports: context -> context -> thm -> thm Seq.seq
    5.57    val exports: context -> context -> thm -> thm Seq.seq
    5.58    val export: context -> context -> thm -> thm
    5.59    val export_standard: context -> context -> thm -> thm
    5.60 -  val drop_schematic: indexname * term option -> indexname * term option
    5.61    val add_binds: (indexname * string option) list -> context -> context
    5.62    val add_binds_i: (indexname * term option) list -> context -> context
    5.63    val auto_bind_goal: term list -> context -> context
    5.64 @@ -141,13 +124,9 @@
    5.65    val add_fixes: (string * string option * mixfix) list -> context -> string list * context
    5.66    val add_fixes_i: (string * typ option * mixfix) list -> context -> string list * context
    5.67    val add_fixes_legacy: (string * typ option * mixfix) list -> context -> string list * context
    5.68 -  val invent_fixes: string list -> context -> string list * context
    5.69    val fix_frees: term -> context -> context
    5.70    val auto_fixes: context * (term list list * 'a) -> context * (term list list * 'a)
    5.71    val bind_fixes: string list -> context -> (term -> term) * context
    5.72 -  val import_types: bool -> typ list -> context -> typ list * context
    5.73 -  val import_terms: bool -> term list -> context -> term list * context
    5.74 -  val import: bool -> thm list -> context -> thm list * context
    5.75    val add_assms: export ->
    5.76      ((string * attribute list) * (string * string list) list) list ->
    5.77      context -> (bstring * thm list) list * context
    5.78 @@ -198,22 +177,15 @@
    5.79     {naming: NameSpace.naming,                     (*local naming conventions*)
    5.80      syntax: LocalSyntax.T,                        (*local syntax*)
    5.81      consts: Consts.T * Consts.T,                  (*global/local consts*)
    5.82 -    fixes: bool * (string * string) list,         (*fixes: !!x. _ with proof body flag*)
    5.83      assms:
    5.84        ((cterm list * export) list *               (*assumes and views: A ==> _*)
    5.85          (string * thm list) list),                (*prems: A |- A*)
    5.86 -    binds: (typ * term) Vartab.table,             (*term bindings*)
    5.87      thms: thm list NameSpace.table * FactIndex.T, (*local thms*)
    5.88 -    cases: (string * (RuleCases.T * bool)) list,  (*local contexts*)
    5.89 -    defaults:
    5.90 -      typ Vartab.table *                          (*type constraints*)
    5.91 -      sort Vartab.table *                         (*default sorts*)
    5.92 -      string list *                               (*used type variables*)
    5.93 -      term list Symtab.table};                    (*type variable occurrences*)
    5.94 +    cases: (string * (RuleCases.T * bool)) list}; (*local contexts*)
    5.95  
    5.96 -fun make_ctxt (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) =
    5.97 -  Ctxt {naming = naming, syntax = syntax, consts = consts, fixes = fixes, assms = assms,
    5.98 -    binds = binds, thms = thms, cases = cases, defaults = defaults};
    5.99 +fun make_ctxt (naming, syntax, consts, assms, thms, cases) =
   5.100 +  Ctxt {naming = naming, syntax = syntax, consts = consts, assms = assms,
   5.101 +    thms = thms, cases = cases};
   5.102  
   5.103  val local_naming = NameSpace.default_naming |> NameSpace.add_path "local";
   5.104  
   5.105 @@ -223,9 +195,8 @@
   5.106    type T = ctxt;
   5.107    fun init thy =
   5.108      make_ctxt (local_naming, LocalSyntax.init thy,
   5.109 -      (Sign.consts_of thy, Sign.consts_of thy), (false, []), ([], []),
   5.110 -      Vartab.empty, (NameSpace.empty_table, FactIndex.empty), [],
   5.111 -      (Vartab.empty, Vartab.empty, [], Symtab.empty));
   5.112 +      (Sign.consts_of thy, Sign.consts_of thy), ([], []),
   5.113 +      (NameSpace.empty_table, FactIndex.empty), []);
   5.114    fun print _ _ = ();
   5.115  );
   5.116  
   5.117 @@ -234,44 +205,32 @@
   5.118  fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
   5.119  
   5.120  fun map_context f =
   5.121 -  ContextData.map (fn Ctxt {naming, syntax, consts, fixes, assms, binds, thms, cases, defaults} =>
   5.122 -    make_ctxt (f (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults)));
   5.123 +  ContextData.map (fn Ctxt {naming, syntax, consts, assms, thms, cases} =>
   5.124 +    make_ctxt (f (naming, syntax, consts, assms, thms, cases)));
   5.125  
   5.126  fun map_naming f =
   5.127 -  map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
   5.128 -    (f naming, syntax, consts, fixes, assms, binds, thms, cases, defaults));
   5.129 +  map_context (fn (naming, syntax, consts, assms, thms, cases) =>
   5.130 +    (f naming, syntax, consts, assms, thms, cases));
   5.131  
   5.132  fun map_syntax f =
   5.133 -  map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
   5.134 -    (naming, f syntax, consts, fixes, assms, binds, thms, cases, defaults));
   5.135 +  map_context (fn (naming, syntax, consts, assms, thms, cases) =>
   5.136 +    (naming, f syntax, consts, assms, thms, cases));
   5.137  
   5.138  fun map_consts f =
   5.139 -  map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
   5.140 -    (naming, syntax, f consts, fixes, assms, binds, thms, cases, defaults));
   5.141 -
   5.142 -fun map_fixes f =
   5.143 -  map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
   5.144 -    (naming, syntax, consts, f fixes, assms, binds, thms, cases, defaults));
   5.145 +  map_context (fn (naming, syntax, consts, assms, thms, cases) =>
   5.146 +    (naming, syntax, f consts, assms, thms, cases));
   5.147  
   5.148  fun map_assms f =
   5.149 -  map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
   5.150 -    (naming, syntax, consts, fixes, f assms, binds, thms, cases, defaults));
   5.151 -
   5.152 -fun map_binds f =
   5.153 -  map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
   5.154 -    (naming, syntax, consts, fixes, assms, f binds, thms, cases, defaults));
   5.155 +  map_context (fn (naming, syntax, consts, assms, thms, cases) =>
   5.156 +    (naming, syntax, consts, f assms, thms, cases));
   5.157  
   5.158  fun map_thms f =
   5.159 -  map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
   5.160 -    (naming, syntax, consts, fixes, assms, binds, f thms, cases, defaults));
   5.161 +  map_context (fn (naming, syntax, consts, assms, thms, cases) =>
   5.162 +    (naming, syntax, consts, assms, f thms, cases));
   5.163  
   5.164  fun map_cases f =
   5.165 -  map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
   5.166 -    (naming, syntax, consts, fixes, assms, binds, thms, f cases, defaults));
   5.167 -
   5.168 -fun map_defaults f =
   5.169 -  map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
   5.170 -    (naming, syntax, consts, fixes, assms, binds, thms, cases, f defaults));
   5.171 +  map_context (fn (naming, syntax, consts, assms, thms, cases) =>
   5.172 +    (naming, syntax, consts, assms, thms, f cases));
   5.173  
   5.174  val naming_of = #naming o rep_context;
   5.175  val full_name = NameSpace.full o naming_of;
   5.176 @@ -283,30 +242,15 @@
   5.177  
   5.178  val consts_of = #2 o #consts o rep_context;
   5.179  
   5.180 -val is_body = #1 o #fixes o rep_context;
   5.181 -fun set_body b = map_fixes (fn (_, fixes) => (b, fixes));
   5.182 -fun restore_body ctxt = set_body (is_body ctxt);
   5.183 -
   5.184 -val fixes_of = #2 o #fixes o rep_context;
   5.185 -val fixed_names_of = map #2 o fixes_of;
   5.186 -
   5.187  val assumptions_of = #1 o #assms o rep_context;
   5.188  val assms_of = map Thm.term_of o maps #1 o assumptions_of;
   5.189  val prems_of = maps #2 o #2 o #assms o rep_context;
   5.190  
   5.191 -val binds_of = #binds o rep_context;
   5.192 -
   5.193  val thms_of = #thms o rep_context;
   5.194  val fact_index_of = #2 o thms_of;
   5.195  
   5.196  val cases_of = #cases o rep_context;
   5.197  
   5.198 -val defaults_of = #defaults o rep_context;
   5.199 -val type_occs_of = #4 o defaults_of;
   5.200 -
   5.201 -fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt);
   5.202 -fun is_known ctxt x = Vartab.defined (#1 (defaults_of ctxt)) (x, ~1) orelse is_fixed ctxt x;
   5.203 -
   5.204  
   5.205  (* transfer *)
   5.206  
   5.207 @@ -385,31 +329,12 @@
   5.208  
   5.209  
   5.210  
   5.211 -(** default sorts and types **)
   5.212 -
   5.213 -val def_sort = Vartab.lookup o #2 o defaults_of;
   5.214 -
   5.215 -fun def_type ctxt pattern xi =
   5.216 -  let val {binds, defaults = (types, _, _, _), ...} = rep_context ctxt in
   5.217 -    (case Vartab.lookup types xi of
   5.218 -      NONE =>
   5.219 -        if pattern then NONE
   5.220 -        else Vartab.lookup binds xi |> Option.map (TypeInfer.polymorphicT o #1)
   5.221 -    | some => some)
   5.222 -  end;
   5.223 -
   5.224 -val used_types = #3 o defaults_of;
   5.225 -
   5.226 -fun default_type ctxt x = Vartab.lookup (#1 (defaults_of ctxt)) (x, ~1);
   5.227 -
   5.228 -
   5.229 -
   5.230  (** prepare types **)
   5.231  
   5.232  local
   5.233  
   5.234  fun read_typ_aux read ctxt s =
   5.235 -  read (syn_of ctxt) (Context.Proof ctxt) (def_sort ctxt) s;
   5.236 +  read (syn_of ctxt) (Context.Proof ctxt) (Variable.def_sort ctxt) s;
   5.237  
   5.238  fun cert_typ_aux cert ctxt raw_T =
   5.239    cert (theory_of ctxt) raw_T handle TYPE (msg, _, _) => error msg;
   5.240 @@ -428,7 +353,7 @@
   5.241  
   5.242  (* internalize Skolem constants *)
   5.243  
   5.244 -val lookup_skolem = AList.lookup (op =) o fixes_of;
   5.245 +val lookup_skolem = AList.lookup (op =) o Variable.fixes_of;
   5.246  fun get_skolem ctxt x = the_default x (lookup_skolem ctxt x);
   5.247  
   5.248  fun no_skolem internal x =
   5.249 @@ -455,7 +380,7 @@
   5.250  (* externalize Skolem constants -- approximation only! *)
   5.251  
   5.252  fun rev_skolem ctxt =
   5.253 -  let val rev_fixes = map Library.swap (fixes_of ctxt)
   5.254 +  let val rev_fixes = map Library.swap (Variable.fixes_of ctxt)
   5.255    in AList.lookup (op =) rev_fixes end;
   5.256  
   5.257  fun revert_skolem ctxt x =
   5.258 @@ -513,17 +438,14 @@
   5.259  fun certify_consts ctxt =
   5.260    Consts.certify (pp ctxt) (tsig_of ctxt) (consts_of ctxt);
   5.261  
   5.262 -fun expand_binds ctxt schematic =
   5.263 -  let
   5.264 -    val binds = binds_of ctxt;
   5.265 +fun reject_schematic (Var (xi, _)) =
   5.266 +      error ("Unbound schematic variable: " ^ Syntax.string_of_vname xi)
   5.267 +  | reject_schematic (Abs (_, _, t)) = reject_schematic t
   5.268 +  | reject_schematic (t $ u) = (reject_schematic t; reject_schematic u)
   5.269 +  | reject_schematic _ = ();
   5.270  
   5.271 -    fun expand_var (xi, T) =
   5.272 -      (case Vartab.lookup binds xi of
   5.273 -        SOME t => Envir.expand_atom T t
   5.274 -      | NONE =>
   5.275 -          if schematic then Var (xi, T)
   5.276 -          else error ("Unbound schematic variable: " ^ Syntax.string_of_vname xi));
   5.277 -  in Envir.beta_norm o Term.map_aterms (fn Var v => expand_var v | a => a) end;
   5.278 +fun expand_binds ctxt schematic =
   5.279 +  Variable.expand_binds ctxt #> (if schematic then I else tap reject_schematic);
   5.280  
   5.281  
   5.282  (* dummy patterns *)
   5.283 @@ -548,9 +470,9 @@
   5.284  fun gen_read' read app pattern schematic
   5.285      ctxt internal more_types more_sorts more_used s =
   5.286    let
   5.287 -    val types = append_env (def_type ctxt pattern) more_types;
   5.288 -    val sorts = append_env (def_sort ctxt) more_sorts;
   5.289 -    val used = used_types ctxt @ more_used;
   5.290 +    val types = append_env (Variable.def_type ctxt pattern) more_types;
   5.291 +    val sorts = append_env (Variable.def_sort ctxt) more_sorts;
   5.292 +    val used = Variable.used_types ctxt @ more_used;
   5.293    in
   5.294      (read (pp ctxt) (syn_of ctxt) ctxt (types, sorts, used) s
   5.295        handle TERM (msg, _) => error msg)
   5.296 @@ -586,8 +508,6 @@
   5.297  
   5.298  (* certify terms *)
   5.299  
   5.300 -val test = ref (NONE: (context * term) option);
   5.301 -
   5.302  local
   5.303  
   5.304  fun gen_cert prop pattern schematic ctxt t = t
   5.305 @@ -609,92 +529,29 @@
   5.306  end;
   5.307  
   5.308  
   5.309 -(* declare types/terms *)
   5.310 -
   5.311 -local
   5.312 -
   5.313 -val ins_types = fold_aterms
   5.314 -  (fn Free (x, T) => Vartab.update ((x, ~1), T)
   5.315 -    | Var v => Vartab.update v
   5.316 -    | _ => I);
   5.317 -
   5.318 -val ins_sorts = fold_atyps
   5.319 -  (fn TFree (x, S) => Vartab.update ((x, ~1), S)
   5.320 -    | TVar v => Vartab.update v
   5.321 -    | _ => I);
   5.322 -
   5.323 -val ins_used = fold_atyps
   5.324 -  (fn TFree (x, _) => insert (op =) x | _ => I);
   5.325 -
   5.326 -val ins_occs = fold_term_types (fn t =>
   5.327 -  fold_atyps (fn TFree (x, _) => Symtab.update_list (x, t) | _ => I));
   5.328 -
   5.329 -fun ins_skolem def_ty = fold_rev (fn (x, x') =>
   5.330 -  (case def_ty x' of
   5.331 -    SOME T => Vartab.update ((x, ~1), T)
   5.332 -  | NONE => I));
   5.333 -
   5.334 -in
   5.335 -
   5.336 -fun declare_type T = map_defaults (fn (types, sorts, used, occ) =>
   5.337 - (types,
   5.338 -  ins_sorts T sorts,
   5.339 -  ins_used T used,
   5.340 -  occ));
   5.341 -
   5.342 -fun declare_syntax t = map_defaults (fn (types, sorts, used, occ) =>
   5.343 - (ins_types t types,
   5.344 -  fold_types ins_sorts t sorts,
   5.345 -  fold_types ins_used t used,
   5.346 -  occ));
   5.347 -
   5.348 -fun declare_var (x, opt_T, mx) ctxt =
   5.349 -  let val T = (case opt_T of SOME T => T | NONE => TypeInfer.mixfixT mx)
   5.350 -  in ((x, T, mx), ctxt |> declare_syntax (Free (x, T))) end;
   5.351 -
   5.352 -fun declare_term t ctxt =
   5.353 -  ctxt
   5.354 -  |> declare_syntax t
   5.355 -  |> map_defaults (fn (types, sorts, used, occ) =>
   5.356 -     (ins_skolem (fn x => Vartab.lookup types (x, ~1)) (fixes_of ctxt) types,
   5.357 -      sorts,
   5.358 -      used,
   5.359 -      ins_occs t occ));
   5.360 -
   5.361 -end;
   5.362 -
   5.363 -
   5.364 -(* invent types *)
   5.365 -
   5.366 -fun invent_types Ss ctxt =
   5.367 -  let
   5.368 -    val tfrees = Term.invent_names (used_types ctxt) "'a" (length Ss) ~~ Ss;
   5.369 -    val ctxt' = fold (declare_type o TFree) tfrees ctxt;
   5.370 -  in (tfrees, ctxt') end;
   5.371 -
   5.372 -
   5.373  (* inferred types of parameters *)
   5.374  
   5.375  fun infer_type ctxt x =
   5.376    (case try (fn () =>
   5.377 -      Sign.infer_types (pp ctxt) (theory_of ctxt) (consts_of ctxt) (def_type ctxt false)
   5.378 -        (def_sort ctxt) (used_types ctxt) true ([Free (x, dummyT)], TypeInfer.logicT)) () of
   5.379 +      Sign.infer_types (pp ctxt) (theory_of ctxt) (consts_of ctxt) (Variable.def_type ctxt false)
   5.380 +        (Variable.def_sort ctxt) (Variable.used_types ctxt) true
   5.381 +        ([Free (x, dummyT)], TypeInfer.logicT)) () of
   5.382      SOME (Free (_, T), _) => T
   5.383    | _ => error ("Failed to infer type of fixed variable " ^ quote x));
   5.384  
   5.385  fun inferred_param x ctxt =
   5.386    let val T = infer_type ctxt x
   5.387 -  in ((x, T), ctxt |> declare_syntax (Free (x, T))) end;
   5.388 +  in ((x, T), ctxt |> Variable.declare_syntax (Free (x, T))) end;
   5.389  
   5.390  fun inferred_fixes ctxt =
   5.391 -  fold_map inferred_param (rev (fixed_names_of ctxt)) ctxt;
   5.392 +  fold_map inferred_param (rev (Variable.fixed_names_of ctxt)) ctxt;
   5.393  
   5.394  
   5.395  (* type and constant names *)
   5.396  
   5.397  fun read_tyname ctxt c =
   5.398 -  if member (op =) (used_types ctxt) c then
   5.399 -    TFree (c, the_default (Sign.defaultS (theory_of ctxt)) (def_sort ctxt (c, ~1)))
   5.400 +  if member (op =) (Variable.used_types ctxt) c then
   5.401 +    TFree (c, the_default (Sign.defaultS (theory_of ctxt)) (Variable.def_sort ctxt (c, ~1)))
   5.402    else Sign.read_tyname (theory_of ctxt) c;
   5.403  
   5.404  fun read_const ctxt c =
   5.405 @@ -703,100 +560,13 @@
   5.406    | NONE => Consts.read_const (consts_of ctxt) c);
   5.407  
   5.408  
   5.409 -(* renaming term/type frees *)
   5.410 -
   5.411 -fun rename_frees ctxt ts frees =
   5.412 -  let
   5.413 -    val (types, sorts, _, _) = defaults_of (ctxt |> fold declare_syntax ts);
   5.414 -    fun rename (x, X) xs =
   5.415 -      let
   5.416 -        fun used y = y = "" orelse y = "'" orelse member (op =) xs y orelse
   5.417 -          Vartab.defined types (y, ~1) orelse Vartab.defined sorts (y, ~1);
   5.418 -        val x' = Term.variant_name used x;
   5.419 -      in ((x', X), x' :: xs) end;
   5.420 -  in #1 (fold_map rename frees []) end;
   5.421 -
   5.422 -
   5.423 -
   5.424 -(** Hindley-Milner polymorphism **)
   5.425 -
   5.426 -(* warn_extra_tfrees *)
   5.427 -
   5.428 -fun warn_extra_tfrees ctxt1 ctxt2 =
   5.429 -  let
   5.430 -    fun occs_typ a (Type (_, Ts)) = exists (occs_typ a) Ts
   5.431 -      | occs_typ a (TFree (b, _)) = a = b
   5.432 -      | occs_typ _ (TVar _) = false;
   5.433 -    fun occs_free a (Free (x, _)) =
   5.434 -          (case def_type ctxt1 false (x, ~1) of
   5.435 -            SOME T => if occs_typ a T then I else cons (a, x)
   5.436 -          | NONE => cons (a, x))
   5.437 -      | occs_free _ _ = I;
   5.438 -
   5.439 -    val occs1 = type_occs_of ctxt1 and occs2 = type_occs_of ctxt2;
   5.440 -    val extras = Symtab.fold (fn (a, ts) =>
   5.441 -      if Symtab.defined occs1 a then I else fold (occs_free a) ts) occs2 [];
   5.442 -    val tfrees = map #1 extras |> sort_distinct string_ord;
   5.443 -    val frees = map #2 extras |> sort_distinct string_ord;
   5.444 -  in
   5.445 -    if null extras then ()
   5.446 -    else warning ("Introduced fixed type variable(s): " ^ commas tfrees ^ " in " ^
   5.447 -      space_implode " or " (map (string_of_term ctxt2 o Syntax.free) frees));
   5.448 -    ctxt2
   5.449 -  end;
   5.450 -
   5.451 -
   5.452 -(* generalize type variables *)
   5.453 -
   5.454 -fun generalize_tfrees inner outer =
   5.455 -  let
   5.456 -    val extra_fixes = subtract (op =) (fixed_names_of outer) (fixed_names_of inner);
   5.457 -    fun still_fixed (Free (x, _)) = not (member (op =) extra_fixes x)
   5.458 -      | still_fixed _ = false;
   5.459 -    val occs_inner = type_occs_of inner;
   5.460 -    val occs_outer = type_occs_of outer;
   5.461 -    fun add a gen =
   5.462 -      if Symtab.defined occs_outer a orelse
   5.463 -        exists still_fixed (Symtab.lookup_list occs_inner a)
   5.464 -      then gen else a :: gen;
   5.465 -  in fn tfrees => fold add tfrees [] end;
   5.466 -
   5.467 -fun generalize inner outer ts =
   5.468 -  let
   5.469 -    val tfrees = generalize_tfrees inner outer (map #1 (fold Term.add_tfrees ts []));
   5.470 -    fun gen (x, S) = if member (op =) tfrees x then TVar ((x, 0), S) else TFree (x, S);
   5.471 -  in map (Term.map_term_types (Term.map_type_tfree gen)) ts end;
   5.472 -
   5.473 -
   5.474 -(* monomorphic vs. polymorphic terms *)
   5.475 -
   5.476 -fun monomorphic_inst ts ctxt =
   5.477 -  let
   5.478 -    val tvars = rev (fold Term.add_tvars ts []);
   5.479 -    val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt;
   5.480 -  in (tvars ~~ map TFree tfrees, ctxt') end;
   5.481 -
   5.482 -fun monomorphic ctxt ts =
   5.483 -  map (Term.instantiate (#1 (monomorphic_inst ts (fold declare_term ts ctxt)), [])) ts;
   5.484 -
   5.485 -fun polymorphic ctxt ts =
   5.486 -  generalize (fold declare_term ts ctxt) ctxt ts;
   5.487 -
   5.488 -fun hidden_polymorphism t T =
   5.489 -  let
   5.490 -    val tvarsT = Term.add_tvarsT T [];
   5.491 -    val extra_tvars = Term.fold_types (Term.fold_atyps
   5.492 -      (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
   5.493 -  in extra_tvars end;
   5.494 -
   5.495 -
   5.496  
   5.497  (** export theorems **)
   5.498  
   5.499  fun common_exports is_goal inner outer =
   5.500    let
   5.501 -    val gen = generalize_tfrees inner outer;
   5.502 -    val fixes = subtract (op =) (fixed_names_of outer) (fixed_names_of inner);
   5.503 +    val gen = Variable.generalize_tfrees inner outer;
   5.504 +    val fixes = subtract (op =) (Variable.fixed_names_of outer) (Variable.fixed_names_of inner);
   5.505      val asms = Library.drop (length (assumptions_of outer), assumptions_of inner);
   5.506      val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms;
   5.507    in
   5.508 @@ -834,30 +604,6 @@
   5.509  
   5.510  (** bindings **)
   5.511  
   5.512 -(* delete_update_binds *)
   5.513 -
   5.514 -local
   5.515 -
   5.516 -val del_bind = map_binds o Vartab.delete_safe;
   5.517 -
   5.518 -fun upd_bind ((x, i), t) =
   5.519 -  let
   5.520 -    val T = Term.fastype_of t;
   5.521 -    val t' =
   5.522 -      if null (hidden_polymorphism t T) then t
   5.523 -      else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T);
   5.524 -  in declare_term t' #> map_binds (Vartab.update ((x, i), (T, t'))) end;
   5.525 -
   5.526 -fun del_upd_bind (xi, NONE) = del_bind xi
   5.527 -  | del_upd_bind (xi, SOME t) = upd_bind (xi, t);
   5.528 -
   5.529 -in
   5.530 -
   5.531 -val delete_update_binds = fold del_upd_bind;
   5.532 -
   5.533 -end;
   5.534 -
   5.535 -
   5.536  (* simult_matches *)
   5.537  
   5.538  fun simult_matches ctxt (t, pats) =
   5.539 @@ -871,7 +617,7 @@
   5.540  local
   5.541  
   5.542  fun gen_bind prep (xi as (x, _), raw_t) ctxt =
   5.543 -  ctxt |> delete_update_binds [(xi, Option.map (prep ctxt) raw_t)];
   5.544 +  ctxt |> Variable.add_binds [(xi, Option.map (prep ctxt) raw_t)];
   5.545  
   5.546  in
   5.547  
   5.548 @@ -894,7 +640,7 @@
   5.549  
   5.550  fun prep_bind prep_pats (raw_pats, t) ctxt =
   5.551    let
   5.552 -    val ctxt' = declare_term t ctxt;
   5.553 +    val ctxt' = Variable.declare_term t ctxt;
   5.554      val pats = prep_pats (Term.fastype_of t) ctxt' raw_pats;
   5.555      val binds = simult_matches ctxt' (t, pats);
   5.556    in (binds, ctxt') end;
   5.557 @@ -905,13 +651,13 @@
   5.558      val (binds, ctxt') =
   5.559        apfst flat (fold_map (prep_bind prep_pats) (map fst raw_binds ~~ ts) ctxt);
   5.560      val binds' =
   5.561 -      if gen then map #1 binds ~~ generalize ctxt' ctxt (map #2 binds)
   5.562 +      if gen then map #1 binds ~~ Variable.generalize ctxt' ctxt (map #2 binds)
   5.563        else binds;
   5.564      val binds'' = map (apsnd SOME) binds';
   5.565      val ctxt'' =
   5.566 -      warn_extra_tfrees ctxt
   5.567 +      tap (Variable.warn_extra_tfrees ctxt)
   5.568         (if gen then
   5.569 -          ctxt (*sic!*) |> fold declare_term (map #2 binds') |> add_binds_i binds''
   5.570 +          ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> add_binds_i binds''
   5.571          else ctxt' |> add_binds_i binds'');
   5.572    in (ts, ctxt'') end;
   5.573  
   5.574 @@ -930,7 +676,7 @@
   5.575  fun prep_propp schematic prep_props prep_pats (context, args) =
   5.576    let
   5.577      fun prep (_, raw_pats) (ctxt, prop :: props) =
   5.578 -          let val ctxt' = declare_term prop ctxt
   5.579 +          let val ctxt' = Variable.declare_term prop ctxt
   5.580            in ((prop, prep_pats ctxt' raw_pats), (ctxt', props)) end
   5.581        | prep _ _ = sys_error "prep_propp";
   5.582      val (propp, (context', _)) = (fold_map o fold_map) prep args
   5.583 @@ -944,7 +690,7 @@
   5.584      val propss = map (map #1) args;
   5.585  
   5.586      (*generalize result: context evaluated now, binds added later*)
   5.587 -    val gen = generalize ctxt' ctxt;
   5.588 +    val gen = Variable.generalize ctxt' ctxt;
   5.589      fun gen_binds c = c |> add_binds_i (map #1 binds ~~ map SOME (gen (map #2 binds)));
   5.590    in (ctxt' |> add_binds_i (map (apsnd SOME) binds), (propss, gen_binds)) end;
   5.591  
   5.592 @@ -1039,7 +785,7 @@
   5.593  fun put_thms _ ("", NONE) ctxt = ctxt
   5.594    | put_thms do_index ("", SOME ths) ctxt = ctxt |> map_thms (fn (facts, index) =>
   5.595        let
   5.596 -        val index' = FactIndex.add_local do_index (is_known ctxt) ("", ths) index;
   5.597 +        val index' = FactIndex.add_local do_index (Variable.is_declared ctxt) ("", ths) index;
   5.598        in (facts, index') end)
   5.599    | put_thms _ (bname, NONE) ctxt = ctxt |> map_thms (fn ((space, tab), index) =>
   5.600        let
   5.601 @@ -1051,7 +797,7 @@
   5.602          val name = full_name ctxt bname;
   5.603          val space' = NameSpace.declare (naming_of ctxt) name space;
   5.604          val tab' = Symtab.update (name, ths) tab;
   5.605 -        val index' = FactIndex.add_local do_index (is_known ctxt) (name, ths) index;
   5.606 +        val index' = FactIndex.add_local do_index (Variable.is_declared ctxt) (name, ths) index;
   5.607        in ((space', tab'), index') end);
   5.608  
   5.609  fun put_thms_internal thms ctxt =
   5.610 @@ -1087,6 +833,10 @@
   5.611  
   5.612  (* variables *)
   5.613  
   5.614 +fun declare_var (x, opt_T, mx) ctxt =
   5.615 +  let val T = (case opt_T of SOME T => T | NONE => TypeInfer.mixfixT mx)
   5.616 +  in ((x, T, mx), ctxt |> Variable.declare_syntax (Free (x, T))) end;
   5.617 +
   5.618  local
   5.619  
   5.620  fun prep_vars prep_typ internal legacy =
   5.621 @@ -1145,14 +895,14 @@
   5.622    let
   5.623      val ([(c, _, mx)], _) = cert_vars [(raw_c, NONE, raw_mx)] ctxt;
   5.624      val c' = Syntax.constN ^ full_name ctxt c;
   5.625 -    val [t] = polymorphic ctxt [cert_term (ctxt |> expand_abbrevs false) raw_t];
   5.626 +    val [t] = Variable.polymorphic ctxt [cert_term (ctxt |> expand_abbrevs false) raw_t];
   5.627      val T = Term.fastype_of t;
   5.628      val _ =
   5.629 -      if null (hidden_polymorphism t T) then ()
   5.630 +      if null (Variable.hidden_polymorphism t T) then ()
   5.631        else error ("Extra type variables on rhs of abbreviation: " ^ quote c);
   5.632    in
   5.633      ctxt
   5.634 -    |> declare_term t
   5.635 +    |> Variable.declare_term t
   5.636      |> map_consts (apsnd
   5.637        (Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), true)))
   5.638      |> map_syntax (LocalSyntax.add_modesyntax (theory_of ctxt) prmode [(false, (c', T, mx))])
   5.639 @@ -1174,20 +924,12 @@
   5.640  
   5.641  fun gen_fixes prep raw_vars ctxt =
   5.642    let
   5.643 -    val thy = theory_of ctxt;
   5.644 -
   5.645 -    val (ys, zs) = split_list (fixes_of ctxt);
   5.646      val (vars, ctxt') = prep raw_vars ctxt;
   5.647 -    val xs = map #1 vars;
   5.648 -    val _ = no_dups ctxt (duplicates (op =) xs);
   5.649 -    val xs' =
   5.650 -      if is_body ctxt then Term.variantlist (map Syntax.skolem xs, zs)
   5.651 -      else (no_dups ctxt (xs inter_string ys); no_dups ctxt (xs inter_string zs); xs);
   5.652 +    val (xs', ctxt'') = Variable.add_fixes (map #1 vars) ctxt';
   5.653    in
   5.654 -    ctxt'
   5.655 -    |> map_fixes (fn (b, fixes) => (b, rev (xs ~~ xs') @ fixes))
   5.656 +    ctxt''
   5.657      |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
   5.658 -    |-> (map_syntax o LocalSyntax.add_syntax thy o map prep_mixfix)
   5.659 +    |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix)
   5.660      |> pair xs'
   5.661    end;
   5.662  
   5.663 @@ -1200,32 +942,24 @@
   5.664  end;
   5.665  
   5.666  
   5.667 -(* invent fixes *)
   5.668 -
   5.669 -fun invent_fixes xs ctxt =
   5.670 -  ctxt
   5.671 -  |> set_body true
   5.672 -  |> add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs)
   5.673 -  ||> restore_body ctxt;
   5.674 -
   5.675 -
   5.676  (* fixes vs. frees *)
   5.677  
   5.678  fun fix_frees t ctxt =
   5.679    let
   5.680 -    fun add (Free (x, T)) = if is_fixed ctxt x then I else insert (op =) (x, SOME T, NoSyn)
   5.681 +    fun add (Free (x, T)) =
   5.682 +          if Variable.is_fixed ctxt x then I else insert (op =) (x, SOME T, NoSyn)
   5.683        | add _ = I;
   5.684      val fixes = rev (fold_aterms add t []);
   5.685    in
   5.686      ctxt
   5.687 -    |> declare_term t
   5.688 -    |> set_body false
   5.689 +    |> Variable.declare_term t
   5.690 +    |> Variable.set_body false
   5.691      |> (snd o add_fixes_i fixes)
   5.692 -    |> restore_body ctxt
   5.693 +    |> Variable.restore_body ctxt
   5.694    end;
   5.695  
   5.696  fun auto_fixes (arg as (ctxt, (propss, x))) =
   5.697 -  if is_body ctxt then arg
   5.698 +  if Variable.is_body ctxt then arg
   5.699    else ((fold o fold) fix_frees propss ctxt, (propss, x));
   5.700  
   5.701  fun bind_fixes xs ctxt =
   5.702 @@ -1241,37 +975,6 @@
   5.703    in (bind, ctxt') end;
   5.704  
   5.705  
   5.706 -(* import -- fixes schematic variables *)
   5.707 -
   5.708 -fun import_inst is_open ts ctxt =
   5.709 -  let
   5.710 -    val (instT, ctxt') = monomorphic_inst ts ctxt;
   5.711 -    val vars = map (apsnd (Term.instantiateT instT)) (rev (fold Term.add_vars ts []));
   5.712 -    val rename = if is_open then I else Syntax.internal;
   5.713 -    val (xs, ctxt'') = invent_fixes (Term.variantlist (map (rename o #1 o #1) vars, [])) ctxt';
   5.714 -    val inst = vars ~~ map Free (xs ~~ map #2 vars);
   5.715 -  in ((instT, inst), ctxt'') end;
   5.716 -
   5.717 -fun import_terms is_open ts ctxt =
   5.718 -  let val (inst, ctxt') = import_inst is_open ts ctxt
   5.719 -  in (map (Term.instantiate inst) ts, ctxt') end;
   5.720 -
   5.721 -fun import_types is_open Ts ctxt =
   5.722 -  import_terms is_open (map Logic.mk_type Ts) ctxt
   5.723 -  |>> map Logic.dest_type;
   5.724 -
   5.725 -fun import is_open ths ctxt =
   5.726 -  let
   5.727 -    val thy = theory_of ctxt;
   5.728 -    val cert = Thm.cterm_of thy;
   5.729 -    val certT = Thm.ctyp_of thy;
   5.730 -    val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
   5.731 -    val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT;
   5.732 -    val inst' = map (fn (v, t) => (cert (Var v), cert t)) inst;
   5.733 -    val ths' = map (Thm.instantiate (instT', inst')) ths;
   5.734 -  in (ths', ctxt') end;
   5.735 -
   5.736 -
   5.737  
   5.738  (** assumptions **)
   5.739  
   5.740 @@ -1302,7 +1005,7 @@
   5.741        |> map_assms (fn (asms, prems) => (asms @ [(new_asms, exp)], prems @ new_prems))
   5.742      val ctxt4 = ctxt3
   5.743        |> put_thms_internal (AutoBind.premsN, SOME (prems_of ctxt3));
   5.744 -  in (map #3 results, warn_extra_tfrees ctxt ctxt4) end;
   5.745 +  in (map #3 results, tap (Variable.warn_extra_tfrees ctxt) ctxt4) end;
   5.746  
   5.747  in
   5.748  
   5.749 @@ -1375,7 +1078,7 @@
   5.750    let
   5.751      val (bind, ctxt') = bind_fixes [x] ctxt;
   5.752      val t = bind (Free (x, T));
   5.753 -  in (t, ctxt' |> declare_syntax t) end;
   5.754 +  in (t, ctxt' |> Variable.declare_syntax t) end;
   5.755  
   5.756  in
   5.757  
   5.758 @@ -1446,7 +1149,7 @@
   5.759  
   5.760  fun pretty_binds ctxt =
   5.761    let
   5.762 -    val binds = binds_of ctxt;
   5.763 +    val binds = Variable.binds_of ctxt;
   5.764      fun prt_bind (xi, (T, t)) = pretty_term_no_abbrevs ctxt (Logic.mk_equals (Var (xi, T), t));
   5.765    in
   5.766      if Vartab.is_empty binds andalso not (! verbose) then []
   5.767 @@ -1521,7 +1224,8 @@
   5.768        if x = x' then Pretty.str x
   5.769        else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
   5.770      val fixes =
   5.771 -      rev (filter_out ((can Syntax.dest_internal orf member (op =) structs) o #1) (fixes_of ctxt));
   5.772 +      rev (filter_out ((can Syntax.dest_internal orf member (op =) structs) o #1)
   5.773 +        (Variable.fixes_of ctxt));
   5.774      val prt_fixes = if null fixes then []
   5.775        else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
   5.776          Pretty.commas (map prt_fix fixes))];
   5.777 @@ -1562,7 +1266,7 @@
   5.778      val prt_defT = prt_atom prt_var prt_typ;
   5.779      val prt_defS = prt_atom prt_varT prt_sort;
   5.780  
   5.781 -    val (types, sorts, used, _) = defaults_of ctxt;
   5.782 +    val (types, sorts, used, _) = Variable.defaults_of ctxt;
   5.783    in
   5.784      verb single (K pretty_thy) @
   5.785      pretty_ctxt ctxt @
     6.1 --- a/src/Pure/Tools/codegen_theorems.ML	Thu Jun 15 18:35:16 2006 +0200
     6.2 +++ b/src/Pure/Tools/codegen_theorems.ML	Thu Jun 15 23:08:54 2006 +0200
     6.3 @@ -604,7 +604,7 @@
     6.4            | _ => raise ERROR "rewrite_rhs")
     6.5        | _ => raise ERROR "rewrite_rhs");
     6.6      fun unvarify thms =
     6.7 -      #1 (ProofContext.import true thms (ProofContext.init thy));
     6.8 +      #1 (Variable.import true thms (ProofContext.init thy));
     6.9      val unfold_thms = Tactic.rewrite true (map (make_eq thy) (the_unfolds thy));
    6.10    in
    6.11      thms
     7.1 --- a/src/Pure/Tools/invoke.ML	Thu Jun 15 18:35:16 2006 +0200
     7.2 +++ b/src/Pure/Tools/invoke.ML	Thu Jun 15 23:08:54 2006 +0200
     7.3 @@ -63,7 +63,7 @@
     7.4        Seq.map (Proof.map_context (fn ctxt =>
     7.5          let
     7.6            val ([res_types, res_params, res_prems], ctxt'') =
     7.7 -            fold_burrow (ProofContext.import false) results ctxt';
     7.8 +            fold_burrow (Variable.import false) results ctxt';
     7.9  
    7.10            val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types;
    7.11            val params'' = map (Thm.term_of o Drule.dest_term) res_params;
    7.12 @@ -99,7 +99,7 @@
    7.13  (* FIXME *)
    7.14  fun read_terms ctxt args =
    7.15    #1 (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] args)
    7.16 -  |> ProofContext.polymorphic ctxt;
    7.17 +  |> Variable.polymorphic ctxt;
    7.18  
    7.19  (* FIXME *)
    7.20  fun cert_terms ctxt args = map fst args;