tuned;
authorwenzelm
Thu Mar 06 10:11:38 2014 +0100 (2014-03-06)
changeset 5594772db54a67152
parent 55929 91f245c23bc5
child 55948 bb21b380f65d
tuned;
src/HOL/Nominal/nominal_induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Wed Mar 05 17:23:28 2014 -0800
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Thu Mar 06 10:11:38 2014 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4    let
     1.5      val tune =
     1.6        if internal then Name.internal
     1.7 -      else fn x => the_default x (try Name.dest_internal x);
     1.8 +      else perhaps (try Name.dest_internal);
     1.9      val n = length xs;
    1.10      fun rename prem =
    1.11        let