adapted to ProofContext.revert_skolem: extra Name.clean required;
authorwenzelm
Thu Apr 17 22:22:23 2008 +0200 (2008-04-17)
changeset 26712e2dcda7b0401
parent 26711 3a478bfa1650
child 26713 1c6181def1d0
adapted to ProofContext.revert_skolem: extra Name.clean required;
src/HOL/Nominal/nominal_induct.ML
src/Tools/induct.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Thu Apr 17 22:22:21 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Thu Apr 17 22:22:23 2008 +0200
     1.3 @@ -92,7 +92,8 @@
     1.4  
     1.5      val finish_rule =
     1.6        split_all_tuples
     1.7 -      #> rename_params_rule true (map (ProofContext.revert_skolem defs_ctxt o fst) avoiding);
     1.8 +      #> rename_params_rule true
     1.9 +        (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding);
    1.10      fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
    1.11    in
    1.12      (fn i => fn st =>
     2.1 --- a/src/Tools/induct.ML	Thu Apr 17 22:22:21 2008 +0200
     2.2 +++ b/src/Tools/induct.ML	Thu Apr 17 22:22:23 2008 +0200
     2.3 @@ -460,7 +460,7 @@
     2.4  
     2.5  fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
     2.6        let
     2.7 -        val x = ProofContext.revert_skolem ctxt z;
     2.8 +        val x = Name.clean (ProofContext.revert_skolem ctxt z);
     2.9          fun index i [] = []
    2.10            | index i (y :: ys) =
    2.11                if x = y then x ^ string_of_int i :: index (i + 1) ys
    2.12 @@ -508,7 +508,7 @@
    2.13      val v = Free (x, T);
    2.14      fun spec_rule prfx (xs, body) =
    2.15        @{thm Pure.meta_spec}
    2.16 -      |> Thm.rename_params_rule ([ProofContext.revert_skolem ctxt x], 1)
    2.17 +      |> Thm.rename_params_rule ([Name.clean (ProofContext.revert_skolem ctxt x)], 1)
    2.18        |> Thm.lift_rule (cert prfx)
    2.19        |> `(Thm.prop_of #> Logic.strip_assums_concl)
    2.20        |-> (fn pred $ arg =>
     3.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Apr 17 22:22:21 2008 +0200
     3.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Apr 17 22:22:23 2008 +0200
     3.3 @@ -341,7 +341,7 @@
     3.4       val quant_induct =
     3.5         Goal.prove_global thy1 [] ind_prems
     3.6           (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
     3.7 -         (fn prems => EVERY
     3.8 +         (fn {prems, ...} => EVERY
     3.9             [rewrite_goals_tac part_rec_defs,
    3.10              rtac (@{thm impI} RS @{thm allI}) 1,
    3.11              DETERM (etac raw_induct 1),
    3.12 @@ -484,7 +484,7 @@
    3.13         if need_mutual then
    3.14           Goal.prove_global thy1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
    3.15             mutual_induct_concl
    3.16 -           (fn prems => EVERY
    3.17 +           (fn {prems, ...} => EVERY
    3.18               [rtac (quant_induct RS lemma) 1,
    3.19                mutual_ind_tac (rev prems) (length prems)])
    3.20         else TrueI;