# 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;