repaired read_const_expr, broken in 1e7ca47c6c3d
authorhaftmann
Mon Dec 07 09:16:27 2009 +0100 (2009-12-07)
changeset 3401358ed621899db
parent 34009 8c0ef28ec159
child 34014 7dd37f4c755b
repaired read_const_expr, broken in 1e7ca47c6c3d
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Sun Dec 06 08:28:36 2009 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Dec 07 09:16:27 2009 +0100
     1.3 @@ -928,9 +928,9 @@
     1.4            | NONE => thy;
     1.5          val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
     1.6            ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
     1.7 -        fun belongs_here c =
     1.8 -          not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
     1.9 -      in if is_some some_thyname then cs else filter belongs_here cs end;
    1.10 +        fun belongs_here c = forall
    1.11 +          (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy')
    1.12 +      in if is_some some_thyname then filter belongs_here cs else cs end;
    1.13      fun read_const_expr "*" = ([], consts_of NONE)
    1.14        | read_const_expr s = if String.isSuffix ".*" s
    1.15            then ([], consts_of (SOME (unsuffix ".*" s)))