changeset 21708 | 45e7491bea47 |
parent 21506 | b2a673894ce5 |
child 21991 | 04528ce9ded5 |
--- a/src/Pure/Tools/nbe.ML Thu Dec 07 21:44:13 2006 +0100 +++ b/src/Pure/Tools/nbe.ML Thu Dec 07 23:16:55 2006 +0100 @@ -78,7 +78,7 @@ let val ctxt = ProofContext.init thy; val posts = (map (LocalDefs.meta_rewrite_rule ctxt) o snd) (NBE_Rewrite.get thy) - in Tactic.rewrite false posts end + in MetaSimplifier.rewrite false posts end (* code store *)