# HG changeset patch
# User haftmann
# Date 1449080097 -3600
# Node ID 029162bc9793e66d4c1d8401662337e8723b499b
# Parent  2256ef8224f6078b34d8c8b351e2f7cdddde7005
prefer conventional read/check distinction over manual check

diff -r 2256ef8224f6 -r 029162bc9793 src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Wed Dec 02 19:14:57 2015 +0100
+++ b/src/Pure/Isar/interpretation.ML	Wed Dec 02 19:14:57 2015 +0100
@@ -52,13 +52,13 @@
 
 local
 
-fun prep_mixins prep_term prep_prop expr_ctxt read_rew_ctxt raw_defs raw_eqns =
+fun prep_mixins prep_term prep_props expr_ctxt read_rew_ctxt raw_defs raw_eqns =
   let
-    val prep = Syntax.check_terms read_rew_ctxt #> Variable.export_terms read_rew_ctxt expr_ctxt;
-    val rhss = (prep o map (prep_term read_rew_ctxt o snd o snd)) raw_defs;
+    val export = Variable.export_terms read_rew_ctxt expr_ctxt;
+    val rhss = (export o map (prep_term read_rew_ctxt o snd o snd)) raw_defs;
     val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
       ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
-    val eqns = (prep o map (prep_prop read_rew_ctxt o snd)) raw_eqns;
+    val eqns = (export o prep_props read_rew_ctxt o map snd) raw_eqns;
   in (pre_defs, eqns) end;
 
 fun define_mixins [] expr_ctxt = ([], expr_ctxt)
@@ -78,12 +78,12 @@
           |> Proof_Context.export inner_def_lthy def_lthy;
       in (def_eqns, Proof_Context.transfer (Proof_Context.theory_of def_lthy) expr_lthy) end;
 
-fun prep_interpretation prep_expr prep_term prep_prop prep_attr
+fun prep_interpretation prep_expr prep_term prep_props prep_attr
   expression raw_defs raw_eqns initial_ctxt =
   let
     val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
     val (pre_defs, eqns) =
-      prep_mixins prep_term prep_prop expr_ctxt
+      prep_mixins prep_term prep_props expr_ctxt
         (fold Locale.activate_declarations deps expr_ctxt) raw_defs raw_eqns;
     val (def_eqns, def_ctxt) = define_mixins pre_defs expr_ctxt;
     val attrss = map (apsnd (map (prep_attr def_ctxt)) o fst) raw_eqns;
@@ -94,11 +94,12 @@
 in
 
 fun cert_interpretation expression =
-  prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I) expression;
+  prep_interpretation Expression.cert_goal_expression Syntax.check_term
+    Syntax.check_props (K I) expression;
 
 fun read_interpretation expression =
-  prep_interpretation Expression.read_goal_expression Syntax.parse_term
-    Syntax.parse_prop Attrib.check_src expression;
+  prep_interpretation Expression.read_goal_expression Syntax.read_term
+    Syntax.read_props Attrib.check_src expression;
 
 end;