# HG changeset patch
# User blanchet
# Date 1234875714 -3600
# Node ID 62f931b257b7fbfba44ed6df3fec51a64a264cdf
# Parent  61837a9bdd74e365be36f5c9e2015813e64ed7cf
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).

diff -r 61837a9bdd74 -r 62f931b257b7 src/HOL/Tools/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 #>