src/Pure/term.ML
changeset 15914 2a8f86685745
parent 15797 a63605582573
child 15954 dd516176043a
equal deleted inserted replaced
15913:530099d1a73c 15914:2a8f86685745
    46   val is_Const: term -> bool
    46   val is_Const: term -> bool
    47   val is_Free: term -> bool
    47   val is_Free: term -> bool
    48   val is_Var: term -> bool
    48   val is_Var: term -> bool
    49   val is_first_order: term -> bool
    49   val is_first_order: term -> bool
    50   val dest_Type: typ -> string * typ list
    50   val dest_Type: typ -> string * typ list
       
    51   val dest_TVar: typ -> indexname * sort
       
    52   val dest_TFree: typ -> string * sort
    51   val dest_Const: term -> string * typ
    53   val dest_Const: term -> string * typ
    52   val dest_Free: term -> string * typ
    54   val dest_Free: term -> string * typ
    53   val dest_Var: term -> indexname * typ
    55   val dest_Var: term -> indexname * typ
    54   val type_of: term -> typ
    56   val type_of: term -> typ
    55   val type_of1: typ list * term -> typ
    57   val type_of1: typ list * term -> typ
   259 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
   261 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
   260 val op ---> = Library.foldr (op -->);
   262 val op ---> = Library.foldr (op -->);
   261 
   263 
   262 fun dest_Type (Type x) = x
   264 fun dest_Type (Type x) = x
   263   | dest_Type T = raise TYPE ("dest_Type", [T], []);
   265   | dest_Type T = raise TYPE ("dest_Type", [T], []);
   264 
   266 fun dest_TVar (TVar x) = x
       
   267   | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
       
   268 fun dest_TFree (TFree x) = x
       
   269   | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
   265 
   270 
   266 (** Discriminators **)
   271 (** Discriminators **)
   267 
   272 
   268 fun is_Bound (Bound _) = true
   273 fun is_Bound (Bound _) = true
   269   | is_Bound _         = false;
   274   | is_Bound _         = false;
   824   | map_term _ _ _ (t as Bound _) = t
   829   | map_term _ _ _ (t as Bound _) = t
   825   | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
   830   | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
   826   | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
   831   | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
   827 
   832 
   828 
   833 
   829 
       
   830 (** TFrees and TVars **)
   834 (** TFrees and TVars **)
   831 
   835 
   832 (*maps  (bs,v)  to   v'::bs    this reverses the identifiers bs*)
   836 (*maps  (bs,v)  to   v'::bs    this reverses the identifiers bs*)
   833 fun add_new_id (bs, c) : string list =  variant bs c  ::  bs;
   837 fun add_new_id (bs, c) : string list =  variant bs c  ::  bs;
   834 
   838