src/Pure/logic.ML
 changeset 19425 e0d7d9373faf parent 19406 410b9d9bf9a1 child 19775 06cb6743adf6
```     1.1 --- a/src/Pure/logic.ML	Thu Apr 13 12:01:02 2006 +0200
1.2 +++ b/src/Pure/logic.ML	Thu Apr 13 12:01:03 2006 +0200
1.3 @@ -27,6 +27,7 @@
1.4    val mk_conjunction_list: term list -> term
1.5    val mk_conjunction_list2: term list list -> term
1.6    val dest_conjunction: term -> term * term
1.7 +  val dest_conjunction_list: term -> term list
1.8    val dest_conjunctions: term -> term list
1.9    val strip_horn: term -> term list * term
1.10    val dest_type: term -> typ
1.11 @@ -166,6 +167,12 @@
1.12  fun dest_conjunction (Const ("ProtoPure.conjunction", _) \$ A \$ B) = (A, B)
1.13    | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
1.14
1.15 +(*A && B && C -- improper*)
1.16 +fun dest_conjunction_list t =
1.17 +  (case try dest_conjunction t of
1.18 +    NONE => [t]
1.19 +  | SOME (A, B) => A :: dest_conjunction_list B);
1.20 +
1.21  (*((A && B) && C) && D && E -- flat*)
1.22  fun dest_conjunctions t =
1.23    (case try dest_conjunction t of
1.24 @@ -327,7 +334,7 @@
1.25
1.26  (*Close up a formula over all free variables by quantification*)
1.27  fun close_form A =
1.28 -  list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A);
1.29 +  Term.list_all_free (rev (Term.add_frees A []), A);
1.30
1.31
1.32
```