# HG changeset patch
# User wenzelm
# Date 1248471397 -7200
# Node ID 678f14c9afb5b00b0329364f38fd13cb202cad67
# Parent  f01207d56583be0cb0693709b3b2855ae6fef354
get_name: cover only PThm, not PAxm;

diff -r f01207d56583 -r 678f14c9afb5 src/Pure/proofterm.ML
--- 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;