# HG changeset patch
# User haftmann
# Date 1293044920 -3600
# Node ID 9400026a82f56379595d3d0407fa3cfd06fce47e
# Parent  6476ab765777f63abf88557c36d8620b4dad477c
tuned comment

diff -r 6476ab765777 -r 9400026a82f5 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Dec 22 14:44:03 2010 +0100
+++ b/src/Pure/simplifier.ML	Wed Dec 22 20:08:40 2010 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
 
 Generic simplifier, suitable for most logics (see also
-meta_simplifier.ML for the actual meta-level rewriting engine).
+raw_simplifier.ML for the actual meta-level rewriting engine).
 *)
 
 signature BASIC_SIMPLIFIER =