src/Pure/Proof/proof_rewrite_rules.ML

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Sat May 08 17:10:27 2010 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sat May 08 16:53:53 2010 +0200
@@ -244,7 +244,7 @@
 fun elim_defs thy r defs prf =
   let
     val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
-    val defnames = map Thm.get_name defs;
+    val defnames = map Thm.derivation_name defs;
     val f = if not r then I else
       let
         val cnames = map (fst o dest_Const o fst) defs';