1.1 --- a/src/HOL/Tools/Qelim/langford.ML	Thu Mar 05 02:32:46 2009 +0100
     1.2 +++ b/src/HOL/Tools/Qelim/langford.ML	Thu Mar 05 08:24:28 2009 +0100
     1.3 @@ -14,9 +14,9 @@
     1.4  val dest_set =
     1.5   let 
     1.6    fun h acc ct = 
     1.7 -   case (term_of ct) of
     1.8 -     Const("{}",_) => acc
     1.9 -   | Const("insert",_)$_$t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct)
    1.10 +   case term_of ct of
    1.11 +     Const (@{const_name Set.empty}, _) => acc
    1.12 +   | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct)
    1.13  in h [] end;
    1.14  
    1.15  fun prove_finite cT u = 
    1.16 @@ -48,11 +48,11 @@
    1.17         in (ne, f) end
    1.18  
    1.19       val qe = case (term_of L, term_of U) of 
    1.20 -      (Const("{}",_),_) =>  
    1.21 +      (Const (@{const_name Set.empty}, _),_) =>  
    1.22          let
    1.23            val (neU,fU) = proveneF U 
    1.24          in simp_rule (transitive ths (dlo_qeth_nolb OF [neU, fU])) end
    1.25 -    | (_,Const("{}",_)) =>  
    1.26 +    | (_,Const (@{const_name Set.empty}, _)) =>  
    1.27          let
    1.28            val (neL,fL) = proveneF L
    1.29          in simp_rule (transitive ths (dlo_qeth_noub OF [neL, fL])) end