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