# HG changeset patch
# User bulwahn
# Date 1350476037 -7200
# Node ID dd2ae15ac74fa05dd249fd6b93d55f13f0ce3bfe
# Parent  cc69be3c8f87e092b13da0fd1ef182dd718a2d03
refined conversion to only react on proper set comprehensions; tuned

diff -r cc69be3c8f87 -r dd2ae15ac74f src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 17 14:13:57 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 17 14:13:57 2012 +0200
@@ -303,7 +303,9 @@
   fun mk_term t =
     let
       val (T, t') = dest_Collect t
-      val (t'', Ts, fp) = HOLogic.strip_psplits t'
+      val (t'', Ts, fp) = case HOLogic.strip_psplits t' of
+          (_, [_], _) => raise TERM("mk_term", [t'])
+        | (t'', Ts, fp) => (t'', Ts, fp)
       val eq = HOLogic.eq_const T $ Bound (length Ts) $
         (HOLogic.mk_ptuple fp (HOLogic.mk_ptupleT fp Ts) (rev (map_index (fn (i, _) => Bound i) Ts)))
     in
@@ -341,7 +343,7 @@
 fun conv ctxt t =
   let
     val ct = cterm_of (Proof_Context.theory_of ctxt) t
-    val prep_eq = (comprehension_conv ctxt then_conv Raw_Simplifier.rewrite true prep_thms) ct 
+    val prep_eq = (comprehension_conv ctxt then_conv Raw_Simplifier.rewrite true prep_thms) ct
     val t' = term_of (Thm.rhs_of prep_eq)
     fun mk_thm (fm, t'') = Goal.prove ctxt [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq (t', t''))) (fn {context, ...} => tac context fm 1)