src/Pure/tactic.ML
changeset 15011 35be762f58f9
parent 15006 107e4dfd3b96
child 15021 6012f983a79f
     1.1 --- a/src/Pure/tactic.ML	Tue Jun 29 11:18:34 2004 +0200
     1.2 +++ b/src/Pure/tactic.ML	Wed Jun 30 00:42:59 2004 +0200
     1.3 @@ -498,7 +498,7 @@
     1.4  val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
     1.5  
     1.6  fun rewrite_goal_tac rews =
     1.7 -  MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews);
     1.8 +  MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.ss_of rews);
     1.9  
    1.10  (*Rewrite throughout proof state. *)
    1.11  fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);