# HG changeset patch
# User wenzelm
# Date 1152613017 -7200
# Node ID c4710df2c953fc7cf585957d3f980fd4d170b205
# Parent  8f3e1ddb50e62f6a184248a3968c7e6baf318330
Name.internal;

diff -r 8f3e1ddb50e6 -r c4710df2c953 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