src/HOL/Nominal/nominal_induct.ML

--- a/src/HOL/Nominal/nominal_induct.ML	Tue Jul 11 12:16:54 2006 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML	Tue Jul 11 12:16:57 2006 +0200
@@ -63,8 +63,8 @@
 fun rename_params_rule internal xs rule =
   let
     val tune =
-      if internal then Term.internal
-      else fn x => the_default x (try Term.dest_internal x);
+      if internal then Name.internal
+      else fn x => the_default x (try Name.dest_internal x);
     val n = length xs;
     fun rename prem =
       let