added head_name_of;
authorwenzelm
Thu Nov 23 20:33:29 2006 +0100 (2006-11-23)
changeset 2149347050cdc1694
parent 21492 c73faa8e98aa
child 21494 a29412af6aa3
added head_name_of;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Thu Nov 23 20:33:28 2006 +0100
     1.2 +++ b/src/Pure/term.ML	Thu Nov 23 20:33:29 2006 +0100
     1.3 @@ -152,6 +152,7 @@
     1.4    val itselfT: typ -> typ
     1.5    val a_itselfT: typ
     1.6    val argument_type_of: term -> typ
     1.7 +  val head_name_of: term -> string
     1.8    val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
     1.9    val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
    1.10    val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
    1.11 @@ -406,6 +407,15 @@
    1.12  fun head_of (f$t) = head_of f
    1.13    | head_of u = u;
    1.14  
    1.15 +fun head_name_of tm =
    1.16 +  (case head_of tm of
    1.17 +    t as Const (c, _) =>
    1.18 +      if NameSpace.is_qualified c then c
    1.19 +      else raise TERM ("Malformed constant name", [t])
    1.20 +  | t as Free (x, _) =>
    1.21 +      if not (NameSpace.is_qualified x) then x
    1.22 +      else raise TERM ("Malformed fixed variable name", [t])
    1.23 +  | t => raise TERM ("No fixed head of term", [t]));
    1.24  
    1.25  (*number of atoms and abstractions in a term*)
    1.26  fun size_of_term tm =