# HG changeset patch
# User wenzelm
# Date 1194385837 -3600
# Node ID 074d4117655849750b95633dfb2e173e5a5e8812
# Parent  c8352b38d47d8d13bac844006ef937bb2db03cd8
read_const/legacy_intern_skolem: cover consts within the local scope;

diff -r c8352b38d47d -r 074d41176558 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Nov 06 22:50:36 2007 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Nov 06 22:50:37 2007 +0100
@@ -475,7 +475,8 @@
   let
     val sko = lookup_skolem ctxt x;
     val is_const = can (Consts.read_const (consts_of ctxt)) x;
-    val is_free = is_some sko orelse not is_const;
+    val is_scoped_const = Variable.is_const ctxt x;
+    val is_free = (is_some sko orelse not is_const) andalso not is_scoped_const;
     val is_internal = internal x;
     val is_declared = is_some (def_type (x, ~1));
     val res =
@@ -483,7 +484,10 @@
       else ((no_skolem false x; ()) handle ERROR msg =>
           legacy_feature (msg ^ ContextPosition.str_of ctxt);
         if is_internal andalso is_declared then SOME x else NONE);
-  in if is_some res then res else if is_declared then SOME x else NONE end;
+  in
+    if is_some res then res
+    else if is_declared andalso not is_scoped_const then SOME x else NONE
+  end;
 
 fun term_context ctxt =
   let val thy = theory_of ctxt in
@@ -622,9 +626,9 @@
   else Sign.read_tyname (theory_of ctxt) c;
 
 fun read_const ctxt c =
-  (case lookup_skolem ctxt c of
-    SOME x => Free (x, infer_type ctxt x)
-  | NONE => Consts.read_const (consts_of ctxt) c);
+  (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
+    (SOME x, false) => Free (x, infer_type ctxt x)
+  | _ => Consts.read_const (consts_of ctxt) c);