src/Tools/Code/code_thingol.ML
changeset 33969 1e7ca47c6c3d
parent 33957 e9afca2118d4
child 33972 daf65be6bfe5
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Nov 30 11:42:49 2009 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Nov 30 12:28:12 2009 +0100
     1.3 @@ -930,10 +930,7 @@
     1.4            ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
     1.5          fun belongs_here c =
     1.6            not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
     1.7 -      in case some_thyname
     1.8 -       of NONE => cs
     1.9 -        | SOME thyname => filter belongs_here cs
    1.10 -      end;
    1.11 +      in if is_some some_thyname then cs else filter belongs_here cs end;
    1.12      fun read_const_expr "*" = ([], consts_of NONE)
    1.13        | read_const_expr s = if String.isSuffix ".*" s
    1.14            then ([], consts_of (SOME (unsuffix ".*" s)))