get_name: cover only PThm, not PAxm;

--- a/src/Pure/proofterm.ML	Fri Jul 24 22:59:28 2009 +0200
+++ b/src/Pure/proofterm.ML	Fri Jul 24 23:36:37 2009 +0200
@@ -1334,8 +1334,7 @@
 fun get_name hyps prop prf =
   let val prop = Logic.list_implies (hyps, prop) in
     (case strip_combt (fst (strip_combP prf)) of
-      (PAxm (name, prop', _), _) => if prop = prop' then name else ""   (* FIXME !? *)
-    | (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else ""
+      (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else ""
     | _ => "")
   end;