--- a/Nominal-General/nominal_library.ML	Sat Sep 18 06:09:43 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Mon Sep 20 21:52:45 2010 +0800
@@ -6,6 +6,8 @@
 
 signature NOMINAL_LIBRARY =
 sig
+  val is_true: term -> bool
+
   val last2: 'a list -> 'a * 'a
 
   val dest_listT: typ -> typ
@@ -87,6 +89,9 @@
 structure Nominal_Library: NOMINAL_LIBRARY =
 struct
 
+fun is_true @{term "Trueprop True"} = true
+  | is_true _ = false 
+
 fun last2 [] = raise Empty
   | last2 [_] = raise Empty
   | last2 [x, y] = (x, y)
@@ -256,7 +261,7 @@
         SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT)
       | mk_size_measure T = size_const T
 
-    val ((_ $ (_ $ rel)) :: tl) = prems_of st
+    val ((_ $ (_ $ rel)) :: _) = prems_of st
     val measure_trm = 
       fastype_of rel 
       |> HOLogic.dest_setT
@@ -324,7 +329,7 @@
  R ... /\ P ...; split_conj_i picks out
  the part R or P part
 *)
-fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ f2) = 
+fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ _) = 
   (case head_of f1 of
      Const (name, _) => if member (op =) names name then SOME f1 else NONE
    | _ => NONE)