src/Pure/logic.ML
changeset 19775 06cb6743adf6
parent 19425 e0d7d9373faf
child 19806 f860b7a98445
     1.1 --- a/src/Pure/logic.ML	Mon Jun 05 21:54:20 2006 +0200
     1.2 +++ b/src/Pure/logic.ML	Mon Jun 05 21:54:21 2006 +0200
     1.3 @@ -48,6 +48,8 @@
     1.4    val protectC: term
     1.5    val protect: term -> term
     1.6    val unprotect: term -> term
     1.7 +  val mk_term: term -> term
     1.8 +  val dest_term: term -> term
     1.9    val occs: term * term -> bool
    1.10    val close_form: term -> term
    1.11    val combound: term * int * int -> term
    1.12 @@ -316,7 +318,7 @@
    1.13  
    1.14  
    1.15  
    1.16 -(** protected propositions **)
    1.17 +(** protected propositions and embedded terms **)
    1.18  
    1.19  val protectC = Const ("prop", propT --> propT);
    1.20  fun protect t = protectC $ t;
    1.21 @@ -325,6 +327,12 @@
    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 +
    1.27 +fun dest_term (Const ("ProtoPure.term", _) $ t) = t
    1.28 +  | dest_term t = raise TERM ("dest_term", [t]);
    1.29 +
    1.30 +
    1.31  
    1.32  (*** Low-level term operations ***)
    1.33