src/Pure/logic.ML
changeset 20883 b432f20a47ca
parent 20630 2010cbb1a941
child 21016 430b35c9cd27
     1.1 --- a/src/Pure/logic.ML	Sat Oct 07 01:31:10 2006 +0200
     1.2 +++ b/src/Pure/logic.ML	Sat Oct 07 01:31:11 2006 +0200
     1.3 @@ -12,10 +12,8 @@
     1.4    val dest_all: term -> typ * term
     1.5    val mk_equals: term * term -> term
     1.6    val dest_equals: term -> term * term
     1.7 -  val is_equals: term -> bool
     1.8    val mk_implies: term * term -> term
     1.9    val dest_implies: term -> term * term
    1.10 -  val is_implies: term -> bool
    1.11    val list_implies: term list * term -> term
    1.12    val strip_imp_prems: term -> term list
    1.13    val strip_imp_concl: term -> term
    1.14 @@ -99,28 +97,20 @@
    1.15    | dest_all t = raise TERM ("dest_all", [t]);
    1.16  
    1.17  
    1.18 -
    1.19  (** equality **)
    1.20  
    1.21 -(*Make an equality.  DOES NOT CHECK TYPE OF u*)
    1.22 -fun mk_equals(t,u) = equals(fastype_of t) $ t $ u;
    1.23 +fun mk_equals (t, u) = Term.equals (Term.fastype_of t) $ t $ u;
    1.24  
    1.25 -fun dest_equals (Const("==",_) $ t $ u)  =  (t,u)
    1.26 -  | dest_equals t = raise TERM("dest_equals", [t]);
    1.27 -
    1.28 -fun is_equals (Const ("==", _) $ _ $ _) = true
    1.29 -  | is_equals _ = false;
    1.30 +fun dest_equals (Const ("==", _) $ t $ u) = (t, u)
    1.31 +  | dest_equals t = raise TERM ("dest_equals", [t]);
    1.32  
    1.33  
    1.34  (** implies **)
    1.35  
    1.36 -fun mk_implies(A,B) = implies $ A $ B;
    1.37 +fun mk_implies (A, B) = implies $ A $ B;
    1.38  
    1.39 -fun dest_implies (Const("==>",_) $ A $ B)  =  (A,B)
    1.40 -  | dest_implies A = raise TERM("dest_implies", [A]);
    1.41 -
    1.42 -fun is_implies (Const ("==>", _) $ _ $ _) = true
    1.43 -  | is_implies _ = false;
    1.44 +fun dest_implies (Const ("==>", _) $ A $ B) = (A, B)
    1.45 +  | dest_implies A = raise TERM ("dest_implies", [A]);
    1.46  
    1.47  
    1.48  (** nested implications **)