src/Pure/Tools/nbe.ML
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 *)