--- a/src/Pure/Isar/interpretation.ML Wed Nov 18 15:23:34 2015 +0000
+++ b/src/Pure/Isar/interpretation.ML Wed Nov 18 17:37:00 2015 +0000
@@ -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;