src/Pure/variable.ML

 Fixed type/term variables and polymorphic term abbreviations.
 *)
 
 signature VARIABLE =
 sig
-  val is_body: Proof.context -> bool
-  val set_body: bool -> Proof.context -> Proof.context
-  val restore_body: Proof.context -> Proof.context -> Proof.context
   val names_of: Proof.context -> Name.context
   val binds_of: Proof.context -> (typ * term) Vartab.table
   val maxidx_of: Proof.context -> int
   val sorts_of: Proof.context -> sort list
   val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table

   val lookup_const: Proof.context -> string -> string option
   val is_const: Proof.context -> string -> bool
   val declare_const: string * string -> Proof.context -> Proof.context
   val next_bound: string * typ -> Proof.context -> term * Proof.context
   val revert_bounds: Proof.context -> term -> term
+  val is_body: Proof.context -> bool
+  val set_body: bool -> Proof.context -> Proof.context
+  val restore_body: Proof.context -> Proof.context -> Proof.context
   val improper_fixes: Proof.context -> Proof.context
   val restore_proper_fixes: Proof.context -> Proof.context -> Proof.context
   val is_improper: Proof.context -> string -> bool
   val is_fixed: Proof.context -> string -> bool
   val newly_fixed: Proof.context -> Proof.context -> string -> bool

 
 type fixes = (string * bool) Name_Space.table;
 val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN;
 
 datatype data = Data of
- {is_body: bool,                        (*inner body mode*)
-  names: Name.context,                  (*type/term variable names*)
+ {names: Name.context,                  (*type/term variable names*)
   consts: string Symtab.table,          (*consts within the local scope*)
   bounds: int * ((string * typ) * string) list,  (*next index, internal name, type, external name*)
   fixes: fixes,                         (*term fixes -- global name space, intern ~> extern*)
   binds: (typ * term) Vartab.table,     (*term bindings*)
   type_occs: string list Symtab.table,  (*type variables -- possibly within term variables*)

   sorts: sort Ord_List.T,               (*declared sort occurrences*)
   constraints:
     typ Vartab.table *                  (*type constraints*)
     sort Vartab.table};                 (*default sorts*)
 
-fun make_data
-    (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =
-  Data {is_body = is_body, names = names, consts = consts, bounds = bounds, fixes = fixes,
-    binds = binds, type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints};
+fun make_data (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =
+  Data {names = names, consts = consts, bounds = bounds, fixes = fixes, binds = binds,
+    type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints};
 
 val empty_data =
-  make_data (false, Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty,
+  make_data (Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty,
     Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty));
 
 structure Data = Proof_Data
 (
   type T = data;
   fun init _ = empty_data;
 );
 
 fun map_data f =
-  Data.map (fn
-      Data {is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} =>
-    make_data
-      (f (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)));
+  Data.map (fn Data {names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} =>
+    make_data (f (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)));
 
 fun map_names f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, f names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (f names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
 
 fun map_consts f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, f consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, f consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
 
 fun map_bounds f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, consts, f bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, consts, f bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
 
 fun map_fixes f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, consts, bounds, f fixes, binds, type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, consts, bounds, f fixes, binds, type_occs, maxidx, sorts, constraints));
 
 fun map_binds f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, consts, bounds, fixes, f binds, type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, consts, bounds, fixes, f binds, type_occs, maxidx, sorts, constraints));
 
 fun map_type_occs f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, consts, bounds, fixes, binds, f type_occs, maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, consts, bounds, fixes, binds, f type_occs, maxidx, sorts, constraints));
 
 fun map_maxidx f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, consts, bounds, fixes, binds, type_occs, f maxidx, sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, consts, bounds, fixes, binds, type_occs, f maxidx, sorts, constraints));
 
 fun map_sorts f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, f sorts, constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, consts, bounds, fixes, binds, type_occs, maxidx, f sorts, constraints));
 
 fun map_constraints f =
-  map_data (fn
-      (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, f constraints));
+  map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+    (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, f constraints));
 
 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
-
-val is_body = #is_body o rep_data;
-
-fun set_body b =
-  map_data (fn (_, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
-    (b, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
-
-fun restore_body ctxt = set_body (is_body ctxt);
 
 val names_of = #names o rep_data;
 val fixes_of = #fixes o rep_data;
 val fixes_space = Name_Space.space_of_table o fixes_of;
 val binds_of = #binds o rep_data;

       in Term.subst_atomic (map2 subst bounds xs) t end);
 
 
 
 (** fixes **)
+
+(* inner body mode *)
+
+val inner_body =
+  Config.bool (Config.declare ("inner_body", @{here}) (K (Config.Bool false)));
+
+fun is_body ctxt = Config.get ctxt inner_body;
+val set_body = Config.put inner_body;
+fun restore_body ctxt = set_body (is_body ctxt);
+
 
 (* proper mode *)
 
 val proper_fixes =
   Config.bool (Config.declare ("proper_fixes", @{here}) (K (Config.Bool true)));