1.1 --- a/src/Pure/Thy/thm_deps.ML	Sat Jan 15 12:42:19 2011 +0100
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Sat Jan 15 12:47:52 2011 +0100
     1.3 @@ -65,15 +65,14 @@
     1.4  
     1.5      val used =
     1.6        Proofterm.fold_body_thms
     1.7 -        (fn (a, prop, _) => a <> "" ? Symtab.insert_list (op =) (a, prop))
     1.8 +        (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
     1.9          (map (Proofterm.strip_thm o Thm.proof_body_of o #1 o #2) new_thms) Symtab.empty;
    1.10  
    1.11 -    fun is_unused (a, th) =
    1.12 -      not (member (op aconv) (Symtab.lookup_list used a) (Thm.prop_of th));
    1.13 +    fun is_unused a = not (Symtab.defined used a);
    1.14  
    1.15      (* groups containing at least one used theorem *)
    1.16 -    val used_groups = fold (fn (a, (th, _, group)) =>
    1.17 -      if is_unused (a, th) then I
    1.18 +    val used_groups = fold (fn (a, (_, _, group)) =>
    1.19 +      if is_unused a then I
    1.20        else
    1.21          (case group of
    1.22            NONE => I
    1.23 @@ -82,7 +81,7 @@
    1.24      val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
    1.25        if not concealed andalso
    1.26          member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.get_kind th) andalso
    1.27 -        is_unused (a, th)
    1.28 +        is_unused a
    1.29        then
    1.30          (case group of
    1.31             NONE => ((a, th) :: thms, seen_groups)