Reintroduce set_interpreter for Collect and op :.
I removed them by accident when removing old code that dealt with the "set" type.
Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).

--- a/src/HOL/Tools/refute.ML	Mon Feb 16 20:33:23 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Tue Feb 17 14:01:54 2009 +0100
@@ -2662,6 +2662,34 @@
   (* theory -> model -> arguments -> Term.term ->
     (interpretation * model * arguments) option *)
 
+  fun set_interpreter thy model args t =
+  let
+    val (typs, terms) = model
+  in
+    case AList.lookup (op =) terms t of
+      SOME intr =>
+      (* return an existing interpretation *)
+      SOME (intr, model, args)
+    | NONE =>
+      (case t of
+      (* 'Collect' == identity *)
+        Const (@{const_name Collect}, _) $ t1 =>
+        SOME (interpret thy model args t1)
+      | Const (@{const_name Collect}, _) =>
+        SOME (interpret thy model args (eta_expand t 1))
+      (* 'op :' == application *)
+      | Const (@{const_name "op :"}, _) $ t1 $ t2 =>
+        SOME (interpret thy model args (t2 $ t1))
+      | Const (@{const_name "op :"}, _) $ t1 =>
+        SOME (interpret thy model args (eta_expand t 1))
+      | Const (@{const_name "op :"}, _) =>
+        SOME (interpret thy model args (eta_expand t 2))
+      | _ => NONE)
+  end;
+
+  (* theory -> model -> arguments -> Term.term ->
+    (interpretation * model * arguments) option *)
+
   (* only an optimization: 'card' could in principle be interpreted with *)
   (* interpreters available already (using its definition), but the code *)
   (* below is more efficient                                             *)
@@ -3271,6 +3299,7 @@
      add_interpreter "stlc"    stlc_interpreter #>
      add_interpreter "Pure"    Pure_interpreter #>
      add_interpreter "HOLogic" HOLogic_interpreter #>
+     add_interpreter "set"     set_interpreter #>
      add_interpreter "IDT"             IDT_interpreter #>
      add_interpreter "IDT_constructor" IDT_constructor_interpreter #>
      add_interpreter "IDT_recursion"   IDT_recursion_interpreter #>