# HG changeset patch
# User wenzelm
# Date 1547401705 -3600
# Node ID aac49f64051d2e727ffe699dfd1de24905766544
# Parent  e4e5bc6ac21471587391c38ccdd4d0b7672dc61d
clarified -- removed pointless Parse.!!!;

diff -r e4e5bc6ac214 -r aac49f64051d src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sun Jan 13 18:40:26 2019 +0100
+++ b/src/Tools/Code/code_target.ML	Sun Jan 13 18:48:25 2019 +0100
@@ -701,10 +701,6 @@
     (Scan.repeat (Parse.name -- (Scan.optional (\<^keyword>\<open>?\<close> >> K false) true) -- code_expr_argsP)))
       >> (fn seri_args => check_code_cmd all_public raw_cs seri_args);
 
-val code_exprP =
-  (Scan.optional (\<^keyword>\<open>open\<close> >> K true) false -- Scan.repeat1 Parse.term)
-    :|-- (fn args => (code_expr_checkingP args || code_expr_inP args));
-
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>code_reserved\<close>
     "declare words as reserved for target language"
@@ -725,6 +721,8 @@
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>export_code\<close> "generate executable code for constants"
-    (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.context_of)));
+    (Scan.optional (\<^keyword>\<open>open\<close> >> K true) false -- Scan.repeat1 Parse.term
+      :|-- (fn args => (code_expr_checkingP args || code_expr_inP args))
+      >> (fn f => Toplevel.keep (f o Toplevel.context_of)));
 
 end; (*struct*)