# HG changeset patch
# User haftmann
# Date 1260173787 -3600
# Node ID 58ed621899dbd49d8164ab3586f55477ccd376be
# Parent  8c0ef28ec1597f43a8ffb77e0bf6fb96eb74802e
repaired read_const_expr, broken in 1e7ca47c6c3d

diff -r 8c0ef28ec159 -r 58ed621899db src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sun Dec 06 08:28:36 2009 +0100
+++ b/src/Tools/Code/code_thingol.ML	Mon Dec 07 09:16:27 2009 +0100
@@ -928,9 +928,9 @@
           | NONE => thy;
         val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
           ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
-        fun belongs_here c =
-          not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
-      in if is_some some_thyname then cs else filter belongs_here cs end;
+        fun belongs_here c = forall
+          (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy')
+      in if is_some some_thyname then filter belongs_here cs else cs end;
     fun read_const_expr "*" = ([], consts_of NONE)
       | read_const_expr s = if String.isSuffix ".*" s
           then ([], consts_of (SOME (unsuffix ".*" s)))