--- a/src/HOL/Nominal/nominal_induct.ML Thu Apr 17 22:22:21 2008 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Thu Apr 17 22:22:23 2008 +0200
@@ -92,7 +92,8 @@
val finish_rule =
split_all_tuples
- #> rename_params_rule true (map (ProofContext.revert_skolem defs_ctxt o fst) avoiding);
+ #> rename_params_rule true
+ (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding);
fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
in
(fn i => fn st =>
--- 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 =>
--- a/src/ZF/Tools/inductive_package.ML Thu Apr 17 22:22:21 2008 +0200
+++ b/src/ZF/Tools/inductive_package.ML Thu Apr 17 22:22:23 2008 +0200
@@ -341,7 +341,7 @@
val quant_induct =
Goal.prove_global thy1 [] ind_prems
(FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
- (fn prems => EVERY
+ (fn {prems, ...} => EVERY
[rewrite_goals_tac part_rec_defs,
rtac (@{thm impI} RS @{thm allI}) 1,
DETERM (etac raw_induct 1),
@@ -484,7 +484,7 @@
if need_mutual then
Goal.prove_global thy1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
mutual_induct_concl
- (fn prems => EVERY
+ (fn {prems, ...} => EVERY
[rtac (quant_induct RS lemma) 1,
mutual_ind_tac (rev prems) (length prems)])
else TrueI;