# HG changeset patch
# User wenzelm
# Date 1146859184 -7200
# Node ID 179ad0076f75102c87fdc46a1b5f86e25923bad5
# Parent  2d9940cd52d3edfe69bafe2d86f5d870479596ea
extern_early: improved handling of undeclared constants;

diff -r 2d9940cd52d3 -r 179ad0076f75 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Fri May 05 21:59:43 2006 +0200
+++ b/src/Pure/consts.ML	Fri May 05 21:59:44 2006 +0200
@@ -113,8 +113,8 @@
 
 fun extern_early consts c =
   (case try (the_const consts) c of
-    SOME (_, true) => extern consts c
-  | _ => Syntax.constN ^ c);
+    SOME (_, false) => Syntax.constN ^ c
+  | _ => extern consts c);
 
 
 (* read_const *)