src/HOL/Nominal/nominal_induct.ML
changeset 20072 c4710df2c953
parent 19903 158ea5884966
child 20288 8ff4a0ea49b2
equal deleted inserted replaced
20071:8f3e1ddb50e6 20072:c4710df2c953
    61   in (((cases, concls), consumes), Drule.cterm_instantiate substs rule) end;
    61   in (((cases, concls), consumes), Drule.cterm_instantiate substs rule) end;
    62 
    62 
    63 fun rename_params_rule internal xs rule =
    63 fun rename_params_rule internal xs rule =
    64   let
    64   let
    65     val tune =
    65     val tune =
    66       if internal then Term.internal
    66       if internal then Name.internal
    67       else fn x => the_default x (try Term.dest_internal x);
    67       else fn x => the_default x (try Name.dest_internal x);
    68     val n = length xs;
    68     val n = length xs;
    69     fun rename prem =
    69     fun rename prem =
    70       let
    70       let
    71         val ps = Logic.strip_params prem;
    71         val ps = Logic.strip_params prem;
    72         val p = length ps;
    72         val p = length ps;