# HG changeset patch
# User wenzelm
# Date 1162664740 -3600
# Node ID 663a7b39894c021ebf8d59e5f0c0297589a4aad4
# Parent  eea3c9048c7aabe3afe63afeefe554da563e2c20
removed is_Trueprop (use can dest_Trueprop'' instead);
tuned list_all;

diff -r eea3c9048c7a -r 663a7b39894c src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Sat Nov 04 19:25:39 2006 +0100
+++ b/src/HOL/hologic.ML	Sat Nov 04 19:25:40 2006 +0100
@@ -17,7 +17,6 @@
   val dest_setT: typ -> typ
   val Trueprop: term
   val mk_Trueprop: term -> term
-  val is_Trueprop: term -> bool
   val dest_Trueprop: term -> term
   val conj: term
   val disj: term
@@ -122,9 +121,6 @@
 
 fun mk_Trueprop P = Trueprop $ P;
 
-fun is_Trueprop (Const ("Trueprop", _) $ _) = true
-  | is_Trueprop t = false;
-
 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
 
@@ -165,7 +161,7 @@
 
 fun all_const T = Const ("All", [T --> boolT] ---> boolT);
 fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
-fun list_all (vs,x) = Library.foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P)) (vs, x);
+fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t;
 
 fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
 fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);