# HG changeset patch # User wenzelm # Date 1208463743 -7200 # Node ID e2dcda7b0401168a4a25daef1ccfed5b5eed99c5 # Parent 3a478bfa165041f796fdc5f9f72438cd02d46d83 adapted to ProofContext.revert_skolem: extra Name.clean required; diff -r 3a478bfa1650 -r e2dcda7b0401 src/HOL/Nominal/nominal_induct.ML --- 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 => diff -r 3a478bfa1650 -r e2dcda7b0401 src/Tools/induct.ML --- 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 => diff -r 3a478bfa1650 -r e2dcda7b0401 src/ZF/Tools/inductive_package.ML --- 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;