src/Pure/tactic.ML
changeset 17892 62c397c17d18
parent 17851 2fa4f9b54761
child 17968 d50f08d9aabb
     1.1 --- a/src/Pure/tactic.ML	Tue Oct 18 17:59:24 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Tue Oct 18 17:59:25 2005 +0200
     1.3 @@ -535,8 +535,10 @@
     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)
     1.8 -    (MetaSimplifier.empty_ss addsimps rews);
     1.9 +  let val ss = MetaSimplifier.empty_ss addsimps rews in
    1.10 +    fn i => fn st => MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac)
    1.11 +      (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
    1.12 +  end;
    1.13  
    1.14  (*Rewrite throughout proof state. *)
    1.15  fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);