# HG changeset patch
# User haftmann
# Date 1293052874 -3600
# Node ID b71bcdb568c05c829c000a926f02ea8d8b4f782c
# Parent  9400026a82f56379595d3d0407fa3cfd06fce47e# Parent  207ee8f8a19ca0af447e3602076742de909689af
merged

diff -r 207ee8f8a19c -r b71bcdb568c0 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Dec 22 22:20:57 2010 +0100
+++ b/src/Pure/simplifier.ML	Wed Dec 22 22:21:14 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 =