# HG changeset patch
# User haftmann
# Date 1334820696 -7200
# Node ID 1e18bbfb40cba024bb8c58078892502ec4159c72
# Parent  1d9faa9f65f95e0ded838b9eee97415d9d1d7b7e
tuned heading

diff -r 1d9faa9f65f9 -r 1e18bbfb40cb src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Wed Apr 18 21:47:26 2012 +0200
+++ b/src/Tools/nbe.ML	Thu Apr 19 09:31:36 2012 +0200
@@ -579,7 +579,7 @@
   in (nbe_program, idx_tab) end;
 
 
-(* dynamic evaluation oracle *)
+(* evaluation oracle *)
 
 fun mk_equals thy lhs raw_rhs =
   let