diff --git a/library/init/lean/ir/extract_cpp.lean b/library/init/lean/ir/extract_cpp.lean
index d253eaacb4..be6e015da6 100644
--- a/library/init/lean/ir/extract_cpp.lean
+++ b/library/init/lean/ir/extract_cpp.lean
@@ -345,7 +345,9 @@ d.foldl (λ s d, match d with
 def emit_used_headers (env : environment) (external_names : fnid → option string) (d : list decl) : except_t format (state_t string id) unit :=
 let used := collect_used d in
 (used.mfor (λ fid, match env fid with
-   | some d := emit_header d.header >> emit ";\n" >> when (need_uncurry d) (emit_uncurry_header d >> emit ";\n")
+   | some d := do
+     unless (external_names fid = none) (emit "extern \"C\" "),
+     emit_header d.header >> emit ";\n" >> when (need_uncurry d) (emit_uncurry_header d >> emit ";\n")
    | _      := return ())).run { external_names := external_names, ctx := mk_context, env := env }
 
 end cpp
diff --git a/library/init/lean/ir/lirc.lean b/library/init/lean/ir/lirc.lean
index e7784c9411..f9659f2de1 100644
--- a/library/init/lean/ir/lirc.lean
+++ b/library/init/lean/ir/lirc.lean
@@ -21,7 +21,7 @@ def parse_input_aux : nat → list decl → fnid2string → parser (list decl ×
 | (n+1) ds m :=
   (eoi >> return (ds.reverse, m))
   <|>
-  (do cid ← (do symbol "[", n ← lexeme $ cpp_identifier, symbol "]", return (some n)) <|> return none,
+  (do cid ← (do symbol "[", n ← lexeme $ c_identifier, symbol "]", return (some n)) <|> return none,
       d ← parse_decl,
       match cid with
       | some cid := parse_input_aux n (d::ds) (m.insert d.name cid)