src/Pure/logic.ML
changeset 26424 a6cad32a27b0
parent 25939 ddea202704b4
child 27334 3f17273766f2
     1.1 --- a/src/Pure/logic.ML	Thu Mar 27 14:41:07 2008 +0100
     1.2 +++ b/src/Pure/logic.ML	Thu Mar 27 14:41:09 2008 +0100
     1.3 @@ -145,7 +145,7 @@
     1.4  (** conjunction **)
     1.5  
     1.6  val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
     1.7 -val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
     1.8 +val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);
     1.9  
    1.10  
    1.11  (*A && B*)
    1.12 @@ -161,7 +161,7 @@
    1.13  
    1.14  
    1.15  (*A && B*)
    1.16 -fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
    1.17 +fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B)
    1.18    | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
    1.19  
    1.20  (*A && B && C -- improper*)
    1.21 @@ -264,9 +264,9 @@
    1.22    | unprotect t = raise TERM ("unprotect", [t]);
    1.23  
    1.24  
    1.25 -fun mk_term t = Const ("ProtoPure.term", Term.fastype_of t --> propT) $ t;
    1.26 +fun mk_term t = Const ("Pure.term", Term.fastype_of t --> propT) $ t;
    1.27  
    1.28 -fun dest_term (Const ("ProtoPure.term", _) $ t) = t
    1.29 +fun dest_term (Const ("Pure.term", _) $ t) = t
    1.30    | dest_term t = raise TERM ("dest_term", [t]);
    1.31  
    1.32