src/Pure/Thy/thm_deps.ML
 changeset 41565 9718c32f9c4e parent 41489 8e2b8649507d child 42473 aca720fb3936
```     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)
```