src/HOL/Tools/Qelim/langford.ML

   val dlo_conv : Proof.context -> cterm -> thm
 end
 
 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 =
      implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)

      fun proveneF S =         
        let val (a,A) = Thm.dest_comb S |>> Thm.dest_arg
            val cT = ctyp_of_term a
            val ne = instantiate' [SOME cT] [SOME a, SOME A] 
                     @{thm insert_not_empty}
-           val f = prove_finite cT (dest_set S)
+           val f = prove_finite cT (HOLogic.dest_set S)
        in (ne, f) end
 
      val qe = case (term_of L, term_of U) of 
       (Const (@{const_name Set.empty}, _),_) =>  
         let