src/HOL/Tools/inductive_package.ML
changeset 5303 22029546d109
parent 5179 819f90f278db
child 5553 ae42b36a50c2
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Aug 12 16:16:49 1998 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Aug 12 16:20:49 1998 +0200
     1.3 @@ -341,14 +341,14 @@
     1.4             HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
     1.5               nth_elem (find_index_eq c cs, preds)))))
     1.6          (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac
     1.7 -           (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
     1.8 +           (map meta_eq [sum_case_Inl, sum_case_Inr]),
     1.9            rtac refl 1])) cs;
    1.10  
    1.11      val induct = prove_goalw_cterm [] (cterm_of sign
    1.12        (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
    1.13          [rtac (impI RS allI) 1,
    1.14           DETERM (etac (mono RS (fp_def RS def_induct)) 1),
    1.15 -         rewrite_goals_tac (map mk_meta_eq (vimage_Int::vimage_simps)),
    1.16 +         rewrite_goals_tac (map meta_eq (vimage_Int::vimage_simps)),
    1.17           fold_goals_tac rec_sets_defs,
    1.18           (*This CollectE and disjE separates out the introduction rules*)
    1.19           REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
    1.20 @@ -356,7 +356,7 @@
    1.21             some premise involves disjunction.*)
    1.22           REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE] 
    1.23                       ORELSE' hyp_subst_tac)),
    1.24 -         rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
    1.25 +         rewrite_goals_tac (map meta_eq [sum_case_Inl, sum_case_Inr]),
    1.26           EVERY (map (fn prem =>
    1.27             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
    1.28  
    1.29 @@ -366,7 +366,7 @@
    1.30           REPEAT (EVERY
    1.31             [REPEAT (resolve_tac [conjI, impI] 1),
    1.32              TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
    1.33 -            rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
    1.34 +            rewrite_goals_tac (map meta_eq [sum_case_Inl, sum_case_Inr]),
    1.35              atac 1])])
    1.36  
    1.37    in standard (split_rule (induct RS lemma))
    1.38 @@ -451,7 +451,7 @@
    1.39        prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';
    1.40      val raw_induct = if no_ind then TrueI else
    1.41        if coind then standard (rule_by_tactic
    1.42 -        (rewrite_tac [mk_meta_eq vimage_Un] THEN
    1.43 +        (rewrite_tac [meta_eq vimage_Un] THEN
    1.44            fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
    1.45        else
    1.46          prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def