Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
extern_early: improved handling of undeclared constants;
authorwenzelm
Fri, 05 May 2006 21:59:44 +0200
changeset 19576 179ad0076f75
parent 19575 2d9940cd52d3
child 19577 fdb3642feb49
extern_early: improved handling of undeclared constants;
src/Pure/consts.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle