# HG changeset patch
# User haftmann
# Date 1236784517 -3600
# Node ID f00b993bda0daf9ea58d2386734351f0fbff6833
# Parent  11e5e8bb28f963d68f1ca6d9d2041177ffe66013
(restored previous version)

diff -r 11e5e8bb28f9 -r f00b993bda0d src/HOL/Tools/Qelim/langford.ML
--- a/src/HOL/Tools/Qelim/langford.ML	Wed Mar 11 15:56:52 2009 +0100
+++ b/src/HOL/Tools/Qelim/langford.ML	Wed Mar 11 16:15:17 2009 +0100
@@ -11,6 +11,14 @@
 structure LangfordQE :LANGFORD_QE = 
 struct
 
+val dest_set =
+ let 
+  fun h acc ct = 
+   case term_of ct of
+     Const (@{const_name Set.empty}, _) => acc
+   | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct)
+in h [] end;
+
 fun prove_finite cT u = 
 let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
     fun ins x th =
@@ -36,7 +44,7 @@
            val cT = ctyp_of_term a
            val ne = instantiate' [SOME cT] [SOME a, SOME A] 
                     @{thm insert_not_empty}
-           val f = prove_finite cT (HOLogic.dest_set S)
+           val f = prove_finite cT (dest_set S)
        in (ne, f) end
 
      val qe = case (term_of L, term_of U) of