src/Pure/term.ML
changeset 15914 2a8f86685745
parent 15797 a63605582573
child 15954 dd516176043a
     1.1 --- a/src/Pure/term.ML	Mon May 02 21:07:21 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Tue May 03 02:44:10 2005 +0200
     1.3 @@ -48,6 +48,8 @@
     1.4    val is_Var: term -> bool
     1.5    val is_first_order: term -> bool
     1.6    val dest_Type: typ -> string * typ list
     1.7 +  val dest_TVar: typ -> indexname * sort
     1.8 +  val dest_TFree: typ -> string * sort
     1.9    val dest_Const: term -> string * typ
    1.10    val dest_Free: term -> string * typ
    1.11    val dest_Var: term -> indexname * typ
    1.12 @@ -261,7 +263,10 @@
    1.13  
    1.14  fun dest_Type (Type x) = x
    1.15    | dest_Type T = raise TYPE ("dest_Type", [T], []);
    1.16 -
    1.17 +fun dest_TVar (TVar x) = x
    1.18 +  | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
    1.19 +fun dest_TFree (TFree x) = x
    1.20 +  | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
    1.21  
    1.22  (** Discriminators **)
    1.23  
    1.24 @@ -826,7 +831,6 @@
    1.25    | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
    1.26  
    1.27  
    1.28 -
    1.29  (** TFrees and TVars **)
    1.30  
    1.31  (*maps  (bs,v)  to   v'::bs    this reverses the identifiers bs*)