1.1 --- a/src/Tools/induct.ML	Wed Apr 27 17:44:06 2011 +0200
     1.2 +++ b/src/Tools/induct.ML	Wed Apr 27 17:58:45 2011 +0200
     1.3 @@ -599,7 +599,7 @@
     1.4  
     1.5  fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
     1.6        let
     1.7 -        val x = Name.clean (Proof_Context.revert_skolem ctxt z);
     1.8 +        val x = Name.clean (Variable.revert_fixed ctxt z);
     1.9          fun index i [] = []
    1.10            | index i (y :: ys) =
    1.11                if x = y then x ^ string_of_int i :: index (i + 1) ys
    1.12 @@ -646,7 +646,7 @@
    1.13      val v = Free (x, T);
    1.14      fun spec_rule prfx (xs, body) =
    1.15        @{thm Pure.meta_spec}
    1.16 -      |> Thm.rename_params_rule ([Name.clean (Proof_Context.revert_skolem ctxt x)], 1)
    1.17 +      |> Thm.rename_params_rule ([Name.clean (Variable.revert_fixed ctxt x)], 1)
    1.18        |> Thm.lift_rule (cert prfx)
    1.19        |> `(Thm.prop_of #> Logic.strip_assums_concl)
    1.20        |-> (fn pred $ arg =>