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;