src/Pure/tactic.ML
changeset 15021 6012f983a79f
parent 15011 35be762f58f9
child 15442 3b75e1b22ff1
     1.1 --- a/src/Pure/tactic.ML	Thu Jul 08 19:32:53 2004 +0200
     1.2 +++ b/src/Pure/tactic.ML	Thu Jul 08 19:33:05 2004 +0200
     1.3 @@ -490,7 +490,7 @@
     1.4  (*** Meta-Rewriting Tactics ***)
     1.5  
     1.6  val simple_prover =
     1.7 -  SINGLE o (fn mss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_mss mss)));
     1.8 +  SINGLE o (fn ss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_ss ss)));
     1.9  
    1.10  val rewrite = MetaSimplifier.rewrite_aux simple_prover;
    1.11  val simplify = MetaSimplifier.simplify_aux simple_prover;
    1.12 @@ -498,7 +498,8 @@
    1.13  val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
    1.14  
    1.15  fun rewrite_goal_tac rews =
    1.16 -  MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.ss_of rews);
    1.17 +  MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac)
    1.18 +    (MetaSimplifier.empty_ss addsimps rews);
    1.19  
    1.20  (*Rewrite throughout proof state. *)
    1.21  fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);