src/HOL/Tools/Qelim/langford.ML

--- a/src/HOL/Tools/Qelim/langford.ML	Tue Jul 28 13:37:08 2009 +0200
+++ b/src/HOL/Tools/Qelim/langford.ML	Tue Jul 28 13:37:09 2009 +0200
@@ -15,7 +15,7 @@
  let 
   fun h acc ct = 
    case term_of ct of
-     Const (@{const_name Set.empty}, _) => acc
+     Const (@{const_name Orderings.bot}, _) => acc
    | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct)
 in h [] end;
 
@@ -48,11 +48,11 @@
        in (ne, f) end
 
      val qe = case (term_of L, term_of U) of 
-      (Const (@{const_name Set.empty}, _),_) =>  
+      (Const (@{const_name Orderings.bot}, _),_) =>  
         let
           val (neU,fU) = proveneF U 
         in simp_rule (transitive ths (dlo_qeth_nolb OF [neU, fU])) end
-    | (_,Const (@{const_name Set.empty}, _)) =>  
+    | (_,Const (@{const_name Orderings.bot}, _)) =>  
         let
           val (neL,fL) = proveneF L
         in simp_rule (transitive ths (dlo_qeth_noub OF [neL, fL])) end