--- a/src/Pure/term.ML Thu Nov 23 20:33:28 2006 +0100
+++ b/src/Pure/term.ML Thu Nov 23 20:33:29 2006 +0100
@@ -152,6 +152,7 @@
val itselfT: typ -> typ
val a_itselfT: typ
val argument_type_of: term -> typ
+ val head_name_of: term -> string
val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
@@ -406,6 +407,15 @@
fun head_of (f$t) = head_of f
| head_of u = u;
+fun head_name_of tm =
+ (case head_of tm of
+ t as Const (c, _) =>
+ if NameSpace.is_qualified c then c
+ else raise TERM ("Malformed constant name", [t])
+ | t as Free (x, _) =>
+ if not (NameSpace.is_qualified x) then x
+ else raise TERM ("Malformed fixed variable name", [t])
+ | t => raise TERM ("No fixed head of term", [t]));
(*number of atoms and abstractions in a term*)
fun size_of_term tm =