diff -r 5aa5a8d6e5b5 -r 6b4c41037649 src/HOL/Library/Case_Converter.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Case_Converter.thy	Sun Dec 30 10:30:41 2018 +0100
@@ -0,0 +1,23 @@
+(* Author: Pascal Stoop, ETH Zurich
+   Author: Andreas Lochbihler, Digital Asset *)
+
+theory Case_Converter
+  imports Main
+begin
+
+subsection \<open>Eliminating pattern matches\<close>
+
+definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
+  [code del]: "missing_pattern_match m f = f ()"
+
+lemma missing_pattern_match_cong [cong]:
+  "m = m' \<Longrightarrow> missing_pattern_match m f = missing_pattern_match m' f"
+  by(rule arg_cong)
+
+lemma missing_pattern_match_code [code_unfold]:
+  "missing_pattern_match = Code.abort"
+  unfolding missing_pattern_match_def Code.abort_def ..
+
+ML_file "case_converter.ML"
+
+end