src/HOL/Tools/datatype_rep_proofs.ML
changeset 26359 6d437bde2f1d
parent 26343 0dd2eab7b296
child 26475 3cc1e48d0ce1
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Mar 20 12:04:54 2008 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Mar 20 12:09:20 2008 +0100
     1.3 @@ -401,7 +401,7 @@
     1.4  
     1.5          val rewrites = map mk_meta_eq iso_char_thms;
     1.6          val inj_thms' = map snd newT_iso_inj_thms @
     1.7 -          map (fn r => r RS injD) inj_thms;
     1.8 +          map (fn r => r RS @{thm injD}) inj_thms;
     1.9  
    1.10          val inj_thm = Goal.prove_global thy5 [] []
    1.11            (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
    1.12 @@ -425,7 +425,7 @@
    1.13                               Lim_inject :: fun_cong :: inj_thms')) 1),
    1.14                           atac 1]))])])])]);
    1.15  
    1.16 -        val inj_thms'' = map (fn r => r RS datatype_injI)
    1.17 +        val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
    1.18                               (split_conj_thm inj_thm);
    1.19  
    1.20          val elem_thm = 
    1.21 @@ -442,7 +442,7 @@
    1.22      val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms
    1.23        ([], map #3 newT_iso_axms) (tl descr);
    1.24      val iso_inj_thms = map snd newT_iso_inj_thms @
    1.25 -      map (fn r => r RS injD) iso_inj_thms_unfolded;
    1.26 +      map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded;
    1.27  
    1.28      (* prove  dt_rep_set_i x --> x : range dt_Rep_i *)
    1.29  
    1.30 @@ -461,7 +461,7 @@
    1.31  
    1.32      (* all the theorems are proved by one single simultaneous induction *)
    1.33  
    1.34 -    val range_eqs = map (fn r => mk_meta_eq (r RS range_ex1_eq))
    1.35 +    val range_eqs = map (fn r => mk_meta_eq (r RS @{thm range_ex1_eq}))
    1.36        iso_inj_thms_unfolded;
    1.37  
    1.38      val iso_thms = if length descr = 1 then [] else
    1.39 @@ -470,7 +470,7 @@
    1.40             [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    1.41              REPEAT (rtac TrueI 1),
    1.42              rewrite_goals_tac (mk_meta_eq choice_eq ::
    1.43 -              symmetric (mk_meta_eq expand_fun_eq) :: range_eqs),
    1.44 +              symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
    1.45              rewrite_goals_tac (map symmetric range_eqs),
    1.46              REPEAT (EVERY
    1.47                [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
    1.48 @@ -495,7 +495,7 @@
    1.49      fun prove_constr_rep_thm eqn =
    1.50        let
    1.51          val inj_thms = map fst newT_iso_inj_thms;
    1.52 -        val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
    1.53 +        val rewrites = @{thm o_def} :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
    1.54        in Goal.prove_global thy5 [] [] eqn (fn _ => EVERY
    1.55          [resolve_tac inj_thms 1,
    1.56           rewrite_goals_tac rewrites,