--- a/src/Tools/induct.ML Thu Apr 17 22:22:21 2008 +0200
+++ b/src/Tools/induct.ML Thu Apr 17 22:22:23 2008 +0200
@@ -460,7 +460,7 @@
fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
let
- val x = ProofContext.revert_skolem ctxt z;
+ val x = Name.clean (ProofContext.revert_skolem ctxt z);
fun index i [] = []
| index i (y :: ys) =
if x = y then x ^ string_of_int i :: index (i + 1) ys
@@ -508,7 +508,7 @@
val v = Free (x, T);
fun spec_rule prfx (xs, body) =
@{thm Pure.meta_spec}
- |> Thm.rename_params_rule ([ProofContext.revert_skolem ctxt x], 1)
+ |> Thm.rename_params_rule ([Name.clean (ProofContext.revert_skolem ctxt x)], 1)
|> Thm.lift_rule (cert prfx)
|> `(Thm.prop_of #> Logic.strip_assums_concl)
|-> (fn pred $ arg =>