tuned;

--- 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