# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1447868220 0
# Node ID 286c1741285c190116311a20e820622f8bc141ba
# Parent  a81dc5c4d6a917067cb020b7b3bd4b42d972246d# Parent  c4a6edbfec49395b44f5be069fbadf9fc41fcd7b
Merge

diff -r a81dc5c4d6a9 -r 286c1741285c src/Pure/Isar/interpretation.ML
--- 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;