simplify

C11-FrontEnd/examples/C2.thy

@@ -376,8 +376,8 @@ subsection \<open>Continuation Calculus with the C Environment: Presentation in
 declare [[C_parser_trace = false]]
 
 ML\<open>
-fun C src = C_Module.C' (C_Module.env (Context.the_generic_context ())) src
-val C' = C_Module.C'
+val C = C_Module.C' NONE
+val C' = C_Module.C' o SOME
 \<close>
 
 C \<comment> \<open>Nesting C code without propagating the C environment\<close> \<open>

C11-FrontEnd/examples/C_paper.thy

@@ -50,17 +50,14 @@ ML\<open>
 val _ = Theory.setup
           (C_Inner_Syntax.command C_Inner_Isar_Cmd.setup' C_Parse.ML_source ("\<simeq>setup", \<^here>, \<^here>))
 
-val C' = C_Module.C'
-
-fun C opt = case opt of NONE => C' (C_Module.env (Context.the_generic_context ()))
-                      | SOME env => C' env
+val C = C_Module.C'
 
 fun C_def dir name _ _ =
   Context.map_theory 
     (C_Inner_Syntax.command'
       (C_Inner_Syntax.drop1
         (C_Scan.Right ( (fn src => fn context =>
-                          C' (C_Stack.Data_Lang.get' context |> #2) src context)
+                          C_Module.C' (SOME (C_Stack.Data_Lang.get' context |> #2)) src context)
                       , dir)))
       C_Parse.C_source
       name)

C11-FrontEnd/src/C_Command.thy

@@ -360,19 +360,25 @@ fun C source =
   exec_eval source
   #> Local_Theory.propagate_ml_env
 
-fun C' env_lang src context =
-  context
-  |> C_Env.empty_env_tree
-  |> C_Context.eval_source'
-       env_lang
-       (fn src => start src context)
-       err
-       accept
-       src
-  |> (fn (_, {context, reports_text, error_lines}) => 
-     tap (fn _ => case error_lines of [] => () | l => warning (cat_lines (rev l)))
-         (C_Stack.Data_Tree.map (curry C_Stack.Data_Tree_Args.merge (reports_text, []))
-                                context))
+val C' =
+  let
+    fun C env_lang src context =
+      context
+      |> C_Env.empty_env_tree
+      |> C_Context.eval_source'
+           env_lang
+           (fn src => start src context)
+           err
+           accept
+           src
+      |> (fn (_, {context, reports_text, error_lines}) => 
+         tap (fn _ => case error_lines of [] => () | l => warning (cat_lines (rev l)))
+             (C_Stack.Data_Tree.map (curry C_Stack.Data_Tree_Args.merge (reports_text, []))
+                                    context))
+  in
+    fn NONE => (fn src => C (env (Context.the_generic_context ())) src)
+     | SOME env_lang => C env_lang
+  end
 
 fun C_export_file (pos, _) lthy =
   let