--- a/src/Tools/nbe.ML Mon Aug 23 11:51:32 2010 +0200+++ b/src/Tools/nbe.ML Mon Aug 23 11:51:33 2010 +0200@@ -6,7 +6,7 @@ signature NBE = sig- val dynamic_eval_conv: cterm -> thm+ val dynamic_eval_conv: conv val dynamic_eval_value: theory -> term -> term datatype Univ =