--- 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 =