src/HOL/Tools/inductive_package.ML
changeset 5149 10f0be29c0d1
parent 5120 f7f5442c934a
child 5179 819f90f278db
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Jul 15 14:19:02 1998 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Jul 15 18:26:15 1998 +0200
     1.3 @@ -274,7 +274,7 @@
     1.4           REPEAT (FIRSTGOAL (eresolve_tac rules1)),
     1.5           REPEAT (FIRSTGOAL (eresolve_tac rules2)),
     1.6           EVERY (map (fn prem =>
     1.7 -           DEPTH_SOLVE_1 (ares_tac (prem::[conjI]) 1)) (tl prems))]))
     1.8 +           DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]))
     1.9        (mk_elims cs cTs params intr_ts)
    1.10  
    1.11    in elims end;
    1.12 @@ -358,7 +358,7 @@
    1.13                       ORELSE' hyp_subst_tac)),
    1.14           rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
    1.15           EVERY (map (fn prem =>
    1.16 -           DEPTH_SOLVE_1 (ares_tac (prem::[conjI, refl]) 1)) prems)]);
    1.17 +           DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
    1.18  
    1.19      val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
    1.20        (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
    1.21 @@ -386,6 +386,9 @@
    1.22      val fp_name = if coind then Sign.intern_const (sign_of Gfp.thy) "gfp"
    1.23        else Sign.intern_const (sign_of Lfp.thy) "lfp";
    1.24  
    1.25 +    val used = foldr add_term_names (intr_ts, []);
    1.26 +    val [sname, xname] = variantlist (["S", "x"], used);
    1.27 +
    1.28      (* transform an introduction rule into a conjunction  *)
    1.29      (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
    1.30      (* is transformed into                                *)
    1.31 @@ -394,22 +397,22 @@
    1.32      fun transform_rule r =
    1.33        let
    1.34          val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
    1.35 -        val idx = length frees;
    1.36 -        val subst = subst_free (cs ~~ (map (mk_vimage cs sumT (Bound (idx + 1))) cs));
    1.37 +        val subst = subst_free
    1.38 +          (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
    1.39          val Const ("op :", _) $ t $ u =
    1.40            HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
    1.41  
    1.42        in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
    1.43          (frees, foldr1 (app HOLogic.conj)
    1.44 -          (((HOLogic.eq_const sumT) $ Bound idx $ (mk_inj cs sumT u t))::
    1.45 +          (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
    1.46              (map (subst o HOLogic.dest_Trueprop)
    1.47                (Logic.strip_imp_prems r))))
    1.48        end
    1.49  
    1.50      (* make a disjunction of all introduction rules *)
    1.51  
    1.52 -    val fp_fun = Abs ("S", setT, (HOLogic.Collect_const sumT) $
    1.53 -      Abs ("x", sumT, foldr1 (app HOLogic.disj) (map transform_rule intr_ts)));
    1.54 +    val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
    1.55 +      absfree (xname, sumT, foldr1 (app HOLogic.disj) (map transform_rule intr_ts)));
    1.56  
    1.57      (* add definiton of recursive sets to theory *)
    1.58