# HG changeset patch
# User dixon
# Date 1115081050 -7200
# Node ID 2a8f8668574540b2e5b4723b8ace981309b54248
# Parent  530099d1a73ce99d78195bbf63c4fa22421135ec
lucas - added dest_TVar and dest_TFree.

diff -r 530099d1a73c -r 2a8f86685745 src/Pure/term.ML
--- a/src/Pure/term.ML	Mon May 02 21:07:21 2005 +0200
+++ b/src/Pure/term.ML	Tue May 03 02:44:10 2005 +0200
@@ -48,6 +48,8 @@
   val is_Var: term -> bool
   val is_first_order: term -> bool
   val dest_Type: typ -> string * typ list
+  val dest_TVar: typ -> indexname * sort
+  val dest_TFree: typ -> string * sort
   val dest_Const: term -> string * typ
   val dest_Free: term -> string * typ
   val dest_Var: term -> indexname * typ
@@ -261,7 +263,10 @@
 
 fun dest_Type (Type x) = x
   | dest_Type T = raise TYPE ("dest_Type", [T], []);
-
+fun dest_TVar (TVar x) = x
+  | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
+fun dest_TFree (TFree x) = x
+  | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
 
 (** Discriminators **)
 
@@ -826,7 +831,6 @@
   | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
 
 
-
 (** TFrees and TVars **)
 
 (*maps  (bs,v)  to   v'::bs    this reverses the identifiers bs*)