equal
deleted
inserted
replaced
321 |
321 |
322 |
322 |
323 |
323 |
324 (** protected propositions and embedded terms **) |
324 (** protected propositions and embedded terms **) |
325 |
325 |
326 val protectC = Const ("prop", propT --> propT); |
326 val protectC = Const ("Pure.prop", propT --> propT); |
327 fun protect t = protectC $ t; |
327 fun protect t = protectC $ t; |
328 |
328 |
329 fun unprotect (Const ("prop", _) $ t) = t |
329 fun unprotect (Const ("Pure.prop", _) $ t) = t |
330 | unprotect t = raise TERM ("unprotect", [t]); |
330 | unprotect t = raise TERM ("unprotect", [t]); |
331 |
331 |
332 |
332 |
333 fun mk_term t = Const ("Pure.term", Term.fastype_of t --> propT) $ t; |
333 fun mk_term t = Const ("Pure.term", Term.fastype_of t --> propT) $ t; |
334 |
334 |