--- a/src/Pure/logic.ML Mon Jun 05 21:54:20 2006 +0200
+++ b/src/Pure/logic.ML Mon Jun 05 21:54:21 2006 +0200
@@ -48,6 +48,8 @@
val protectC: term
val protect: term -> term
val unprotect: term -> term
+ val mk_term: term -> term
+ val dest_term: term -> term
val occs: term * term -> bool
val close_form: term -> term
val combound: term * int * int -> term
@@ -316,7 +318,7 @@
-(** protected propositions **)
+(** protected propositions and embedded terms **)
val protectC = Const ("prop", propT --> propT);
fun protect t = protectC $ t;
@@ -325,6 +327,12 @@
| unprotect t = raise TERM ("unprotect", [t]);
+fun mk_term t = Const ("ProtoPure.term", Term.fastype_of t --> propT) $ t;
+
+fun dest_term (Const ("ProtoPure.term", _) $ t) = t
+ | dest_term t = raise TERM ("dest_term", [t]);
+
+
(*** Low-level term operations ***)