# HG changeset patch
# User wenzelm
# Date 1144922463 -7200
# Node ID e0d7d9373faf17b02b391bb1b689980d7a99bd10
# Parent  b701ea590259679b7b04bc931c0928ff67f99a56
added dest_conjunction_list;
close_form: canonical order of variables;

diff -r b701ea590259 -r e0d7d9373faf src/Pure/logic.ML
--- a/src/Pure/logic.ML	Thu Apr 13 12:01:02 2006 +0200
+++ b/src/Pure/logic.ML	Thu Apr 13 12:01:03 2006 +0200
@@ -27,6 +27,7 @@
   val mk_conjunction_list: term list -> term
   val mk_conjunction_list2: term list list -> term
   val dest_conjunction: term -> term * term
+  val dest_conjunction_list: term -> term list
   val dest_conjunctions: term -> term list
   val strip_horn: term -> term list * term
   val dest_type: term -> typ
@@ -166,6 +167,12 @@
 fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
   | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
 
+(*A && B && C -- improper*)
+fun dest_conjunction_list t =
+  (case try dest_conjunction t of
+    NONE => [t]
+  | SOME (A, B) => A :: dest_conjunction_list B);
+
 (*((A && B) && C) && D && E -- flat*)
 fun dest_conjunctions t =
   (case try dest_conjunction t of
@@ -327,7 +334,7 @@
 
 (*Close up a formula over all free variables by quantification*)
 fun close_form A =
-  list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A);
+  Term.list_all_free (rev (Term.add_frees A []), A);