# HG changeset patch
# User wenzelm
# Date 1447853325 -3600
# Node ID c4a6edbfec49395b44f5be069fbadf9fc41fcd7b
# Parent  0753dd4c9144b514a3066feef6e26a6ba8e511a5
make SML/NJ happy;

diff -r 0753dd4c9144 -r c4a6edbfec49 src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Wed Nov 18 10:12:37 2015 +0100
+++ b/src/Pure/Isar/interpretation.ML	Wed Nov 18 14:28:45 2015 +0100
@@ -88,11 +88,12 @@
 
 in
 
-val cert_interpretation =
-  prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I);
+fun cert_interpretation expression =
+  prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I) expression;
 
-val read_interpretation =
-  prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src;
+fun read_interpretation expression =
+  prep_interpretation Expression.read_goal_expression Syntax.parse_term
+    Syntax.parse_prop Attrib.check_src expression;
 
 end;