# HG changeset patch
# User bulwahn
# Date 1294643929 -3600
# Node ID 2110405ed53b399169fbbed2146aec5ba7211a5a
# Parent  e7c1248e39d08cfef8b0ed90d6d1355db6794d63
removing dead code; tuned

diff -r e7c1248e39d0 -r 2110405ed53b src/HOL/Tools/list_to_set_comprehension.ML
--- a/src/HOL/Tools/list_to_set_comprehension.ML	Mon Jan 10 08:18:48 2011 +0100
+++ b/src/HOL/Tools/list_to_set_comprehension.ML	Mon Jan 10 08:18:49 2011 +0100
@@ -13,13 +13,8 @@
 structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
 struct
 
-fun CONVERSION' cv i st = Seq.single (Conv.gconv_rule cv i st)
-
 (* conversion *)
 
-fun trace_conv cv ct =
-  (tracing (Syntax.string_of_term_global @{theory} (Thm.term_of ct)); cv ct)
-
 fun all_exists_conv cv ctxt ct =
   case Thm.term_of ct of
     Const(@{const_name HOL.Ex}, _) $ Abs(_, _, _) =>
@@ -179,12 +174,12 @@
           if eqs = [] then NONE (* no rewriting, nothing to be done *)
           else
             let
-              val Type ("List.list", [rT]) = fastype_of t
+              val Type (@{type_name List.list}, [rT]) = fastype_of t
               val pat_eq =
                 case try dest_singleton_list t of
                   SOME t' => Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool})
                     $ Bound (length bound_vs) $ t'
-                | NONE => Const ("Set.member", rT --> HOLogic.mk_setT rT --> @{typ bool})
+                | NONE => Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool})
                   $ Bound (length bound_vs) $ (mk_set rT $ t)
               val reverse_bounds = curry subst_bounds
                 ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])