more antiquotations;
authorwenzelm
Sun Feb 28 22:30:51 2010 +0100 (2010-02-28)
changeset 354095c5bb83f2bae
parent 35408 b48ab741683b
child 35410 1ea89d2a1bd4
more antiquotations;
eliminated legacy ML bindings;
src/CCL/CCL.thy
src/CCL/Type.thy
src/FOL/IFOL.thy
src/ZF/Datatype_ZF.thy
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
src/ZF/Tools/typechk.ML
src/ZF/UNITY/Constrains.thy
src/ZF/UNITY/SubstAx.thy
src/ZF/arith_data.ML
src/ZF/int_arith.ML
src/ZF/simpdata.ML
     1.1 --- a/src/CCL/CCL.thy	Sat Feb 27 23:13:01 2010 +0100
     1.2 +++ b/src/CCL/CCL.thy	Sun Feb 28 22:30:51 2010 +0100
     1.3 @@ -193,7 +193,7 @@
     1.4        fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})]
     1.5        val inj_lemmas = maps mk_inj_lemmas rews
     1.6      in
     1.7 -      CHANGED (REPEAT (ares_tac [iffI, allI, conjI] i ORELSE
     1.8 +      CHANGED (REPEAT (ares_tac [@{thm iffI}, @{thm allI}, @{thm conjI}] i ORELSE
     1.9          eresolve_tac inj_lemmas i ORELSE
    1.10          asm_simp_tac (simpset_of ctxt addsimps rews) i))
    1.11      end;
    1.12 @@ -242,7 +242,7 @@
    1.13    val eq_lemma = thm "eq_lemma";
    1.14    val distinctness = thm "distinctness";
    1.15    fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL
    1.16 -                           [distinctness RS notE,sym RS (distinctness RS notE)]
    1.17 +                           [distinctness RS notE, @{thm sym} RS (distinctness RS notE)]
    1.18  in
    1.19    fun mk_lemmas rls = maps mk_lemma (mk_combs pair rls)
    1.20    fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs
    1.21 @@ -258,7 +258,7 @@
    1.22    let
    1.23      fun mk_raw_dstnct_thm rls s =
    1.24        Goal.prove_global @{theory} [] [] (Syntax.read_prop_global @{theory} s)
    1.25 -        (fn _=> rtac notI 1 THEN eresolve_tac rls 1)
    1.26 +        (fn _=> rtac @{thm notI} 1 THEN eresolve_tac rls 1)
    1.27    in map (mk_raw_dstnct_thm caseB_lemmas)
    1.28      (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end
    1.29  
    1.30 @@ -406,9 +406,9 @@
    1.31    "~ false [= lam x. f(x)"
    1.32    "~ lam x. f(x) [= false"
    1.33    by (tactic {*
    1.34 -    REPEAT (rtac notI 1 THEN
    1.35 +    REPEAT (rtac @{thm notI} 1 THEN
    1.36        dtac @{thm case_pocong} 1 THEN
    1.37 -      etac rev_mp 5 THEN
    1.38 +      etac @{thm rev_mp} 5 THEN
    1.39        ALLGOALS (simp_tac @{simpset}) THEN
    1.40        REPEAT (resolve_tac [@{thm po_refl}, @{thm npo_lam_bot}] 1)) *})
    1.41  
     2.1 --- a/src/CCL/Type.thy	Sat Feb 27 23:13:01 2010 +0100
     2.2 +++ b/src/CCL/Type.thy	Sun Feb 28 22:30:51 2010 +0100
     2.3 @@ -127,7 +127,7 @@
     2.4  fun mk_ncanT_tac top_crls crls =
     2.5    SUBPROOF (fn {context = ctxt, prems = major :: prems, ...} =>
     2.6      resolve_tac ([major] RL top_crls) 1 THEN
     2.7 -    REPEAT_SOME (eresolve_tac (crls @ [exE, @{thm bexE}, conjE, disjE])) THEN
     2.8 +    REPEAT_SOME (eresolve_tac (crls @ [@{thm exE}, @{thm bexE}, @{thm conjE}, @{thm disjE}])) THEN
     2.9      ALLGOALS (asm_simp_tac (simpset_of ctxt)) THEN
    2.10      ALLGOALS (ares_tac (prems RL [@{thm lem}]) ORELSE' etac @{thm bspec}) THEN
    2.11      safe_tac (claset_of ctxt addSIs prems))
    2.12 @@ -498,7 +498,7 @@
    2.13  fun EQgen_tac ctxt rews i =
    2.14   SELECT_GOAL
    2.15     (TRY (safe_tac (claset_of ctxt)) THEN
    2.16 -    resolve_tac ((rews @ [refl]) RL ((rews @ [refl]) RL [@{thm ssubst_pair}])) i THEN
    2.17 +    resolve_tac ((rews @ [@{thm refl}]) RL ((rews @ [@{thm refl}]) RL [@{thm ssubst_pair}])) i THEN
    2.18      ALLGOALS (simp_tac (simpset_of ctxt)) THEN
    2.19      ALLGOALS EQgen_raw_tac) i
    2.20  *}
     3.1 --- a/src/FOL/IFOL.thy	Sat Feb 27 23:13:01 2010 +0100
     3.2 +++ b/src/FOL/IFOL.thy	Sun Feb 28 22:30:51 2010 +0100
     3.3 @@ -890,45 +890,4 @@
     3.4  lemma all_conj_distrib:
     3.5    "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))" by iprover
     3.6  
     3.7 -
     3.8 -subsection {* Legacy ML bindings *}
     3.9 -
    3.10 -ML {*
    3.11 -val refl = @{thm refl}
    3.12 -val trans = @{thm trans}
    3.13 -val sym = @{thm sym}
    3.14 -val subst = @{thm subst}
    3.15 -val ssubst = @{thm ssubst}
    3.16 -val conjI = @{thm conjI}
    3.17 -val conjE = @{thm conjE}
    3.18 -val conjunct1 = @{thm conjunct1}
    3.19 -val conjunct2 = @{thm conjunct2}
    3.20 -val disjI1 = @{thm disjI1}
    3.21 -val disjI2 = @{thm disjI2}
    3.22 -val disjE = @{thm disjE}
    3.23 -val impI = @{thm impI}
    3.24 -val impE = @{thm impE}
    3.25 -val mp = @{thm mp}
    3.26 -val rev_mp = @{thm rev_mp}
    3.27 -val TrueI = @{thm TrueI}
    3.28 -val FalseE = @{thm FalseE}
    3.29 -val iff_refl = @{thm iff_refl}
    3.30 -val iff_trans = @{thm iff_trans}
    3.31 -val iffI = @{thm iffI}
    3.32 -val iffE = @{thm iffE}
    3.33 -val iffD1 = @{thm iffD1}
    3.34 -val iffD2 = @{thm iffD2}
    3.35 -val notI = @{thm notI}
    3.36 -val notE = @{thm notE}
    3.37 -val allI = @{thm allI}
    3.38 -val allE = @{thm allE}
    3.39 -val spec = @{thm spec}
    3.40 -val exI = @{thm exI}
    3.41 -val exE = @{thm exE}
    3.42 -val eq_reflection = @{thm eq_reflection}
    3.43 -val iff_reflection = @{thm iff_reflection}
    3.44 -val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
    3.45 -val meta_eq_to_iff = @{thm meta_eq_to_iff}
    3.46 -*}
    3.47 -
    3.48  end
     4.1 --- a/src/ZF/Datatype_ZF.thy	Sat Feb 27 23:13:01 2010 +0100
     4.2 +++ b/src/ZF/Datatype_ZF.thy	Sun Feb 28 22:30:51 2010 +0100
     4.3 @@ -92,7 +92,7 @@
     4.4           else ();
     4.5         val goal = Logic.mk_equals (old, new)
     4.6         val thm = Goal.prove (Simplifier.the_context ss) [] [] goal
     4.7 -         (fn _ => rtac iff_reflection 1 THEN
     4.8 +         (fn _ => rtac @{thm iff_reflection} 1 THEN
     4.9             simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
    4.10           handle ERROR msg =>
    4.11           (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term_global sg goal);
     5.1 --- a/src/ZF/Tools/datatype_package.ML	Sat Feb 27 23:13:01 2010 +0100
     5.2 +++ b/src/ZF/Tools/datatype_package.ML	Sun Feb 28 22:30:51 2010 +0100
     5.3 @@ -281,7 +281,7 @@
     5.4          list_comb (case_free, args)));
     5.5  
     5.6    val case_trans = hd con_defs RS @{thm def_trans}
     5.7 -  and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS @{thm trans};
     5.8 +  and split_trans = Pr.split_eq RS @{thm meta_eq_to_obj_eq} RS @{thm trans};
     5.9  
    5.10    fun prove_case_eqn (arg, con_def) =
    5.11      Goal.prove_global thy1 [] []
    5.12 @@ -290,7 +290,9 @@
    5.13        (fn _ => EVERY
    5.14          [rewrite_goals_tac [con_def],
    5.15           rtac case_trans 1,
    5.16 -         REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]);
    5.17 +         REPEAT
    5.18 +           (resolve_tac [@{thm refl}, split_trans,
    5.19 +             Su.case_inl RS @{thm trans}, Su.case_inr RS @{thm trans}] 1)]);
    5.20  
    5.21    val free_iffs = map Drule.export_without_context (con_defs RL [@{thm def_swap_iff}]);
    5.22  
    5.23 @@ -321,7 +323,7 @@
    5.24                           args)),
    5.25               subst_rec (Term.betapplys (recursor_case, args))));
    5.26  
    5.27 -        val recursor_trans = recursor_def RS @{thm def_Vrecursor} RS trans;
    5.28 +        val recursor_trans = recursor_def RS @{thm def_Vrecursor} RS @{thm trans};
    5.29  
    5.30          fun prove_recursor_eqn arg =
    5.31            Goal.prove_global thy1 [] []
     6.1 --- a/src/ZF/Tools/induct_tacs.ML	Sat Feb 27 23:13:01 2010 +0100
     6.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sun Feb 28 22:30:51 2010 +0100
     6.3 @@ -136,7 +136,7 @@
     6.4             rec_rewrites = recursor_eqns,
     6.5             case_rewrites = case_eqns,
     6.6             induct = induct,
     6.7 -           mutual_induct = TrueI,  (*No need for mutual induction*)
     6.8 +           mutual_induct = @{thm TrueI},  (*No need for mutual induction*)
     6.9             exhaustion = elim};
    6.10  
    6.11      val con_info =
     7.1 --- a/src/ZF/Tools/inductive_package.ML	Sat Feb 27 23:13:01 2010 +0100
     7.2 +++ b/src/ZF/Tools/inductive_package.ML	Sun Feb 28 22:30:51 2010 +0100
     7.3 @@ -222,7 +222,7 @@
     7.4       rtac disjIn 2,
     7.5       (*Not ares_tac, since refl must be tried before equality assumptions;
     7.6         backtracking may occur if the premises have extra variables!*)
     7.7 -     DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 2 APPEND assume_tac 2),
     7.8 +     DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac 2),
     7.9       (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
    7.10       rewrite_goals_tac con_defs,
    7.11       REPEAT (rtac @{thm refl} 2),
    7.12 @@ -310,7 +310,7 @@
    7.13         Intro rules with extra Vars in premises still cause some backtracking *)
    7.14       fun ind_tac [] 0 = all_tac
    7.15         | ind_tac(prem::prems) i =
    7.16 -             DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN ind_tac prems (i-1);
    7.17 +             DEPTH_SOLVE_1 (ares_tac [prem, @{thm refl}] i) THEN ind_tac prems (i-1);
    7.18  
    7.19       val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT);
    7.20  
    7.21 @@ -332,7 +332,7 @@
    7.22             setSolver (mk_solver "minimal"
    7.23                        (fn prems => resolve_tac (triv_rls@prems)
    7.24                                     ORELSE' assume_tac
    7.25 -                                   ORELSE' etac FalseE));
    7.26 +                                   ORELSE' etac @{thm FalseE}));
    7.27  
    7.28       val quant_induct =
    7.29         Goal.prove_global thy1 [] ind_prems
    7.30 @@ -470,11 +470,11 @@
    7.31                        (mut_ss addsimps @{thms conj_simps} @ @{thms imp_simps} @ @{thms quant_simps}) 1
    7.32                     THEN
    7.33                     (*unpackage and use "prem" in the corresponding place*)
    7.34 -                   REPEAT (rtac impI 1)  THEN
    7.35 +                   REPEAT (rtac @{thm impI} 1)  THEN
    7.36                     rtac (rewrite_rule all_defs prem) 1  THEN
    7.37                     (*prem must not be REPEATed below: could loop!*)
    7.38 -                   DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE'
    7.39 -                                           eresolve_tac (conjE::mp::cmonos))))
    7.40 +                   DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE'
    7.41 +                                           eresolve_tac (@{thm conjE} :: @{thm mp} :: cmonos))))
    7.42                 ) i)
    7.43              THEN mutual_ind_tac prems (i-1);
    7.44  
    7.45 @@ -485,7 +485,7 @@
    7.46             (fn {prems, ...} => EVERY
    7.47               [rtac (quant_induct RS lemma) 1,
    7.48                mutual_ind_tac (rev prems) (length prems)])
    7.49 -       else TrueI;
    7.50 +       else @{thm TrueI};
    7.51  
    7.52       (** Uncurrying the predicate in the ordinary induction rule **)
    7.53  
    7.54 @@ -498,7 +498,7 @@
    7.55                                        cterm_of thy1 elem_tuple)]);
    7.56  
    7.57       (*strip quantifier and the implication*)
    7.58 -     val induct0 = inst (quant_induct RS spec RSN (2, @{thm rev_mp}));
    7.59 +     val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp}));
    7.60  
    7.61       val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = concl_of induct0
    7.62  
    7.63 @@ -521,7 +521,7 @@
    7.64      else
    7.65        (thy1
    7.66        |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])]
    7.67 -      |> apfst hd |> Library.swap, TrueI)
    7.68 +      |> apfst hd |> Library.swap, @{thm TrueI})
    7.69    and defs = big_rec_def :: part_rec_defs
    7.70  
    7.71  
     8.1 --- a/src/ZF/Tools/primrec_package.ML	Sat Feb 27 23:13:01 2010 +0100
     8.2 +++ b/src/ZF/Tools/primrec_package.ML	Sun Feb 28 22:30:51 2010 +0100
     8.3 @@ -175,7 +175,7 @@
     8.4      val eqn_thms =
     8.5        eqn_terms |> map (fn t =>
     8.6          Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
     8.7 -          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]));
     8.8 +          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac @{thm refl} 1]));
     8.9  
    8.10      val (eqn_thms', thy2) =
    8.11        thy1
     9.1 --- a/src/ZF/Tools/typechk.ML	Sat Feb 27 23:13:01 2010 +0100
     9.2 +++ b/src/ZF/Tools/typechk.ML	Sun Feb 28 22:30:51 2010 +0100
     9.3 @@ -98,7 +98,7 @@
     9.4  (*Instantiates variables in typing conditions.
     9.5    drawback: does not simplify conjunctions*)
     9.6  fun type_solver_tac ctxt hyps = SELECT_GOAL
     9.7 -    (DEPTH_SOLVE (etac FalseE 1
     9.8 +    (DEPTH_SOLVE (etac @{thm FalseE} 1
     9.9                    ORELSE basic_res_tac 1
    9.10                    ORELSE (ares_tac hyps 1
    9.11                            APPEND typecheck_step_tac (tcset_of ctxt))));
    10.1 --- a/src/ZF/UNITY/Constrains.thy	Sat Feb 27 23:13:01 2010 +0100
    10.2 +++ b/src/ZF/UNITY/Constrains.thy	Sun Feb 28 22:30:51 2010 +0100
    10.3 @@ -484,9 +484,9 @@
    10.4                REPEAT (force_tac css 2),
    10.5                full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1,
    10.6                ALLGOALS (clarify_tac cs),
    10.7 -              REPEAT (FIRSTGOAL (etac disjE)),
    10.8 +              REPEAT (FIRSTGOAL (etac @{thm disjE})),
    10.9                ALLGOALS (clarify_tac cs),
   10.10 -              REPEAT (FIRSTGOAL (etac disjE)),
   10.11 +              REPEAT (FIRSTGOAL (etac @{thm disjE})),
   10.12                ALLGOALS (clarify_tac cs),
   10.13                ALLGOALS (asm_full_simp_tac ss),
   10.14                ALLGOALS (clarify_tac cs)])
    11.1 --- a/src/ZF/UNITY/SubstAx.thy	Sat Feb 27 23:13:01 2010 +0100
    11.2 +++ b/src/ZF/UNITY/SubstAx.thy	Sun Feb 28 22:30:51 2010 +0100
    11.3 @@ -366,7 +366,7 @@
    11.4                (* proving the domain part *)
    11.5               clarify_tac cs 3, dtac @{thm swap} 3, force_tac css 4,
    11.6               rtac @{thm ReplaceI} 3, force_tac css 3, force_tac css 4,
    11.7 -             asm_full_simp_tac ss 3, rtac conjI 3, simp_tac ss 4,
    11.8 +             asm_full_simp_tac ss 3, rtac @{thm conjI} 3, simp_tac ss 4,
    11.9               REPEAT (rtac @{thm state_update_type} 3),
   11.10               constrains_tac ctxt 1,
   11.11               ALLGOALS (clarify_tac cs),
    12.1 --- a/src/ZF/arith_data.ML	Sat Feb 27 23:13:01 2010 +0100
    12.2 +++ b/src/ZF/arith_data.ML	Sun Feb 28 22:30:51 2010 +0100
    12.3 @@ -163,9 +163,9 @@
    12.4    val prove_conv = prove_conv "nateq_cancel_numerals"
    12.5    val mk_bal   = FOLogic.mk_eq
    12.6    val dest_bal = FOLogic.dest_eq
    12.7 -  val bal_add1 = @{thm eq_add_iff} RS iff_trans
    12.8 -  val bal_add2 = @{thm eq_add_iff} RS iff_trans
    12.9 -  fun trans_tac _ = gen_trans_tac iff_trans
   12.10 +  val bal_add1 = @{thm eq_add_iff} RS @{thm iff_trans}
   12.11 +  val bal_add2 = @{thm eq_add_iff} RS @{thm iff_trans}
   12.12 +  fun trans_tac _ = gen_trans_tac @{thm iff_trans}
   12.13    end;
   12.14  
   12.15  structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData);
   12.16 @@ -176,9 +176,9 @@
   12.17    val prove_conv = prove_conv "natless_cancel_numerals"
   12.18    val mk_bal   = FOLogic.mk_binrel "Ordinal.lt"
   12.19    val dest_bal = FOLogic.dest_bin "Ordinal.lt" iT
   12.20 -  val bal_add1 = @{thm less_add_iff} RS iff_trans
   12.21 -  val bal_add2 = @{thm less_add_iff} RS iff_trans
   12.22 -  fun trans_tac _ = gen_trans_tac iff_trans
   12.23 +  val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans}
   12.24 +  val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans}
   12.25 +  fun trans_tac _ = gen_trans_tac @{thm iff_trans}
   12.26    end;
   12.27  
   12.28  structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData);
   12.29 @@ -189,9 +189,9 @@
   12.30    val prove_conv = prove_conv "natdiff_cancel_numerals"
   12.31    val mk_bal   = FOLogic.mk_binop "Arith.diff"
   12.32    val dest_bal = FOLogic.dest_bin "Arith.diff" iT
   12.33 -  val bal_add1 = @{thm diff_add_eq} RS trans
   12.34 -  val bal_add2 = @{thm diff_add_eq} RS trans
   12.35 -  fun trans_tac _ = gen_trans_tac trans
   12.36 +  val bal_add1 = @{thm diff_add_eq} RS @{thm trans}
   12.37 +  val bal_add2 = @{thm diff_add_eq} RS @{thm trans}
   12.38 +  fun trans_tac _ = gen_trans_tac @{thm trans}
   12.39    end;
   12.40  
   12.41  structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData);
    13.1 --- a/src/ZF/int_arith.ML	Sat Feb 27 23:13:01 2010 +0100
    13.2 +++ b/src/ZF/int_arith.ML	Sun Feb 28 22:30:51 2010 +0100
    13.3 @@ -128,7 +128,7 @@
    13.4  
    13.5  (*To evaluate binary negations of coefficients*)
    13.6  val zminus_simps = @{thms NCons_simps} @
    13.7 -                   [@{thm integ_of_minus} RS sym,
    13.8 +                   [@{thm integ_of_minus} RS @{thm sym},
    13.9                      @{thm bin_minus_1}, @{thm bin_minus_0}, @{thm bin_minus_Pls}, @{thm bin_minus_Min},
   13.10                      @{thm bin_pred_1}, @{thm bin_pred_0}, @{thm bin_pred_Pls}, @{thm bin_pred_Min}];
   13.11  
   13.12 @@ -144,7 +144,7 @@
   13.13  
   13.14  (*combine unary minus with numeric literals, however nested within a product*)
   13.15  val int_mult_minus_simps =
   13.16 -    [@{thm zmult_assoc}, @{thm zmult_zminus} RS sym, int_minus_mult_eq_1_to_2];
   13.17 +    [@{thm zmult_assoc}, @{thm zmult_zminus} RS @{thm sym}, int_minus_mult_eq_1_to_2];
   13.18  
   13.19  fun prep_simproc thy (name, pats, proc) =
   13.20    Simplifier.simproc thy name pats proc;
   13.21 @@ -156,7 +156,7 @@
   13.22    val mk_coeff          = mk_coeff
   13.23    val dest_coeff        = dest_coeff 1
   13.24    val find_first_coeff  = find_first_coeff []
   13.25 -  fun trans_tac _       = ArithData.gen_trans_tac iff_trans
   13.26 +  fun trans_tac _       = ArithData.gen_trans_tac @{thm iff_trans}
   13.27  
   13.28    val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac}
   13.29    val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
   13.30 @@ -179,8 +179,8 @@
   13.31    val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
   13.32    val mk_bal   = FOLogic.mk_eq
   13.33    val dest_bal = FOLogic.dest_eq
   13.34 -  val bal_add1 = @{thm eq_add_iff1} RS iff_trans
   13.35 -  val bal_add2 = @{thm eq_add_iff2} RS iff_trans
   13.36 +  val bal_add1 = @{thm eq_add_iff1} RS @{thm iff_trans}
   13.37 +  val bal_add2 = @{thm eq_add_iff2} RS @{thm iff_trans}
   13.38  );
   13.39  
   13.40  structure LessCancelNumerals = CancelNumeralsFun
   13.41 @@ -188,8 +188,8 @@
   13.42    val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
   13.43    val mk_bal   = FOLogic.mk_binrel @{const_name "zless"}
   13.44    val dest_bal = FOLogic.dest_bin @{const_name "zless"} @{typ i}
   13.45 -  val bal_add1 = @{thm less_add_iff1} RS iff_trans
   13.46 -  val bal_add2 = @{thm less_add_iff2} RS iff_trans
   13.47 +  val bal_add1 = @{thm less_add_iff1} RS @{thm iff_trans}
   13.48 +  val bal_add2 = @{thm less_add_iff2} RS @{thm iff_trans}
   13.49  );
   13.50  
   13.51  structure LeCancelNumerals = CancelNumeralsFun
   13.52 @@ -197,8 +197,8 @@
   13.53    val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
   13.54    val mk_bal   = FOLogic.mk_binrel @{const_name "zle"}
   13.55    val dest_bal = FOLogic.dest_bin @{const_name "zle"} @{typ i}
   13.56 -  val bal_add1 = @{thm le_add_iff1} RS iff_trans
   13.57 -  val bal_add2 = @{thm le_add_iff2} RS iff_trans
   13.58 +  val bal_add1 = @{thm le_add_iff1} RS @{thm iff_trans}
   13.59 +  val bal_add2 = @{thm le_add_iff2} RS @{thm iff_trans}
   13.60  );
   13.61  
   13.62  val cancel_numerals =
   13.63 @@ -232,9 +232,9 @@
   13.64    val dest_sum          = dest_sum
   13.65    val mk_coeff          = mk_coeff
   13.66    val dest_coeff        = dest_coeff 1
   13.67 -  val left_distrib      = @{thm left_zadd_zmult_distrib} RS trans
   13.68 +  val left_distrib      = @{thm left_zadd_zmult_distrib} RS @{thm trans}
   13.69    val prove_conv        = prove_conv_nohyps "int_combine_numerals"
   13.70 -  fun trans_tac _       = ArithData.gen_trans_tac trans
   13.71 +  fun trans_tac _       = ArithData.gen_trans_tac @{thm trans}
   13.72  
   13.73    val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys
   13.74    val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
   13.75 @@ -274,14 +274,14 @@
   13.76    fun mk_coeff(k,t) = if t=one then mk_numeral k
   13.77                        else raise TERM("mk_coeff", [])
   13.78    fun dest_coeff t = (dest_numeral t, one)  (*We ONLY want pure numerals.*)
   13.79 -  val left_distrib      = @{thm zmult_assoc} RS sym RS trans
   13.80 +  val left_distrib      = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans}
   13.81    val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
   13.82 -  fun trans_tac _       = ArithData.gen_trans_tac trans
   13.83 +  fun trans_tac _       = ArithData.gen_trans_tac @{thm trans}
   13.84  
   13.85  
   13.86  
   13.87  val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps
   13.88 -  val norm_ss2 = ZF_ss addsimps [@{thm zmult_zminus_right} RS sym] @
   13.89 +  val norm_ss2 = ZF_ss addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @
   13.90      bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys
   13.91    fun norm_tac ss =
   13.92      ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
    14.1 --- a/src/ZF/simpdata.ML	Sat Feb 27 23:13:01 2010 +0100
    14.2 +++ b/src/ZF/simpdata.ML	Sun Feb 28 22:30:51 2010 +0100
    14.3 @@ -32,9 +32,9 @@
    14.4  (*Analyse a rigid formula*)
    14.5  val ZF_conn_pairs =
    14.6    [("Ball",     [@{thm bspec}]),
    14.7 -   ("All",      [spec]),
    14.8 -   ("op -->",   [mp]),
    14.9 -   ("op &",     [conjunct1,conjunct2])];
   14.10 +   ("All",      [@{thm spec}]),
   14.11 +   ("op -->",   [@{thm mp}]),
   14.12 +   ("op &",     [@{thm conjunct1}, @{thm conjunct2}])];
   14.13  
   14.14  (*Analyse a:b, where b is rigid*)
   14.15  val ZF_mem_pairs =