# HG changeset patch
# User wenzelm
# Date 1394097098 -3600
# Node ID 72db54a67152d4e8a8d785706f54137ee3600133
# Parent  91f245c23bc540fad6cf04df9e5c8433bce79fce
tuned;

diff -r 91f245c23bc5 -r 72db54a67152 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Wed Mar 05 17:23:28 2014 -0800
+++ b/src/HOL/Nominal/nominal_induct.ML	Thu Mar 06 10:11:38 2014 +0100
@@ -63,7 +63,7 @@
   let
     val tune =
       if internal then Name.internal
-      else fn x => the_default x (try Name.dest_internal x);
+      else perhaps (try Name.dest_internal);
     val n = length xs;
     fun rename prem =
       let