Nominal/nominal_dt_rawfuns.ML
changeset 2571 f0252365936c
parent 2569 94750b31a97d
child 2598 b136721eedb2
--- a/Nominal/nominal_dt_rawfuns.ML	Mon Nov 15 08:17:11 2010 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Mon Nov 15 09:52:29 2010 +0000
@@ -145,12 +145,6 @@
     else raise TERM ("listify", [t])
   end
 
-(* coerces a list into a set *)
-fun to_set t =
-  if fastype_of t = @{typ "atom list"}
-  then @{term "set :: atom list => atom set"} $ t
-  else t
-
 
 (** functions that construct the equations for fv and fv_bn **)