src/Pure/Isar/expression.ML
changeset 41228 e1fce873b814
parent 39557 fe5722fce758
child 41270 dea60d052923
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Dec 17 16:25:21 2010 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Dec 17 17:08:56 2010 +0100
     1.3 @@ -647,18 +647,18 @@
     1.4      val cert = Thm.cterm_of defs_thy;
     1.5  
     1.6      val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
     1.7 -      MetaSimplifier.rewrite_goals_tac [pred_def] THEN
     1.8 +      rewrite_goals_tac [pred_def] THEN
     1.9        Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
    1.10        Tactic.compose_tac (false,
    1.11          Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
    1.12  
    1.13      val conjuncts =
    1.14        (Drule.equal_elim_rule2 OF [body_eq,
    1.15 -        MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
    1.16 +        Raw_Simplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
    1.17        |> Conjunction.elim_balanced (length ts);
    1.18      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
    1.19        Element.prove_witness defs_ctxt t
    1.20 -       (MetaSimplifier.rewrite_goals_tac defs THEN
    1.21 +       (rewrite_goals_tac defs THEN
    1.22          Tactic.compose_tac (false, ax, 0) 1));
    1.23    in ((statement, intro, axioms), defs_thy) end;
    1.24