author | wenzelm |
Tue, 11 Jul 2006 12:16:57 +0200 | |
changeset 20072 | c4710df2c953 |
parent 20071 | 8f3e1ddb50e6 |
child 20073 | da82b545d2de |
--- 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