# HG changeset patch
# User wenzelm
# Date 1164310409 -3600
# Node ID 47050cdc169430fa871be61ebdb8a9760177a841
# Parent  c73faa8e98aa85a623a1ddb374e6da01e54b1c69
added head_name_of;

diff -r c73faa8e98aa -r 47050cdc1694 src/Pure/term.ML
--- 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 =