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