--- 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