diff -r 040519ec99e9 -r b52e8651591f Nominal/nominal_induct.ML
--- a/Nominal/nominal_induct.ML	Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/nominal_induct.ML	Thu Mar 13 09:21:31 2014 +0000
@@ -66,7 +66,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