Name.internal;
authorwenzelm
Tue Jul 11 12:16:57 2006 +0200 (2006-07-11)
changeset 20072c4710df2c953
parent 20071 8f3e1ddb50e6
child 20073 da82b545d2de
Name.internal;
src/HOL/Nominal/nominal_induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Tue Jul 11 12:16:54 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Tue Jul 11 12:16:57 2006 +0200
     1.3 @@ -63,8 +63,8 @@
     1.4  fun rename_params_rule internal xs rule =
     1.5    let
     1.6      val tune =
     1.7 -      if internal then Term.internal
     1.8 -      else fn x => the_default x (try Term.dest_internal x);
     1.9 +      if internal then Name.internal
    1.10 +      else fn x => the_default x (try Name.dest_internal x);
    1.11      val n = length xs;
    1.12      fun rename prem =
    1.13        let