refined notion of consts within the local scope;

--- a/src/Pure/variable.ML	Wed Nov 07 16:42:56 2007 +0100
+++ b/src/Pure/variable.ML	Wed Nov 07 16:42:57 2007 +0100
@@ -31,8 +31,9 @@
   val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
   val add_binds: (indexname * term option) list -> Proof.context -> Proof.context
   val expand_binds: Proof.context -> term -> term
+  val lookup_const: Proof.context -> string -> string option
   val is_const: Proof.context -> string -> bool
-  val declare_const: string -> Proof.context -> Proof.context
+  val declare_const: string * string -> Proof.context -> Proof.context
   val add_fixes: string list -> Proof.context -> string list * Proof.context
   val add_fixes_direct: string list -> Proof.context -> Proof.context
   val auto_fixes: term -> Proof.context -> Proof.context
@@ -70,7 +71,7 @@
 datatype data = Data of
  {is_body: bool,                        (*inner body mode*)
   names: Name.context,                  (*type/term variable names*)
-  scope: bool Symtab.table,             (*local scope of fixes/consts*)
+  consts: string Symtab.table,          (*consts within the local scope*)
   fixes: (string * string) list,        (*term fixes -- extern/intern*)
   binds: (typ * term) Vartab.table,     (*term bindings*)
   type_occs: string list Symtab.table,  (*type variables -- possibly within term variables*)
@@ -79,8 +80,8 @@
     typ Vartab.table *                  (*type constraints*)
     sort Vartab.table};                 (*default sorts*)
 
-fun make_data (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =
-  Data {is_body = is_body, names = names, scope = scope, fixes = fixes, binds = binds,
+fun make_data (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =
+  Data {is_body = is_body, names = names, consts = consts, fixes = fixes, binds = binds,
     type_occs = type_occs, maxidx = maxidx, constraints = constraints};
 
 structure Data = ProofDataFun
@@ -92,43 +93,43 @@
 );
 
 fun map_data f =
-  Data.map (fn Data {is_body, names, scope, fixes, binds, type_occs, maxidx, constraints} =>
-    make_data (f (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints)));
+  Data.map (fn Data {is_body, names, consts, fixes, binds, type_occs, maxidx, constraints} =>
+    make_data (f (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints)));
 
 fun map_names f =
-  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
-    (is_body, f names, scope, fixes, binds, type_occs, maxidx, constraints));
+  map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
+    (is_body, f names, consts, fixes, binds, type_occs, maxidx, constraints));
 
-fun map_scope f =
-  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
-    (is_body, names, f scope, fixes, binds, type_occs, maxidx, constraints));
+fun map_consts f =
+  map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
+    (is_body, names, f consts, fixes, binds, type_occs, maxidx, constraints));
 
 fun map_fixes f =
-  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
-    (is_body, names, scope, f fixes, binds, type_occs, maxidx, constraints));
+  map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
+    (is_body, names, consts, f fixes, binds, type_occs, maxidx, constraints));
 
 fun map_binds f =
-  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
-    (is_body, names, scope, fixes, f binds, type_occs, maxidx, constraints));
+  map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
+    (is_body, names, consts, fixes, f binds, type_occs, maxidx, constraints));
 
 fun map_type_occs f =
-  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
-    (is_body, names, scope, fixes, binds, f type_occs, maxidx, constraints));
+  map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
+    (is_body, names, consts, fixes, binds, f type_occs, maxidx, constraints));
 
 fun map_maxidx f =
-  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
-    (is_body, names, scope, fixes, binds, type_occs, f maxidx, constraints));
+  map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
+    (is_body, names, consts, fixes, binds, type_occs, f maxidx, constraints));
 
 fun map_constraints f =
-  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
-    (is_body, names, scope, fixes, binds, type_occs, maxidx, f constraints));
+  map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
+    (is_body, names, consts, fixes, binds, type_occs, maxidx, f constraints));
 
 fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
 
 val is_body = #is_body o rep_data;
 
-fun set_body b = map_data (fn (_, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
-  (b, names, scope, fixes, binds, type_occs, maxidx, constraints));
+fun set_body b = map_data (fn (_, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
+  (b, names, consts, fixes, binds, type_occs, maxidx, constraints));
 
 fun restore_body ctxt = set_body (is_body ctxt);
 
@@ -255,12 +256,13 @@
 
 
 
-(** local scope **)
+(** consts **)
 
-fun is_const ctxt x = the_default false (Symtab.lookup (#scope (rep_data ctxt)) x);
+val lookup_const = Symtab.lookup o #consts o rep_data;
+val is_const = is_some oo lookup_const;
 
-fun declare_fixed x = map_scope (Symtab.update (x, false));
-fun declare_const c = map_scope (Symtab.update (c, true));
+val declare_fixed = map_consts o Symtab.delete_safe;
+val declare_const = map_consts o Symtab.update;