# HG changeset patch
# User Andreas Lochbihler
# Date 1546162241 -3600
# Node ID 6b4c4103764991980b0037658b8d7cccfb88b8c4
# Parent  5aa5a8d6e5b57ae8b0fa92b0bbf48d1958e1bc4f
separate case converter into a separate theory

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
diff -r 5aa5a8d6e5b5 -r 6b4c41037649 src/HOL/Library/Code_Lazy.thy
--- a/src/HOL/Library/Code_Lazy.thy	Sat Dec 29 20:32:09 2018 +0100
+++ b/src/HOL/Library/Code_Lazy.thy	Sun Dec 30 10:30:41 2018 +0100
@@ -4,7 +4,7 @@
 section \<open>Lazy types in generated code\<close>
 
 theory Code_Lazy
-imports Main
+imports Case_Converter
 keywords
   "code_lazy_type"
   "activate_lazy_type"
@@ -24,22 +24,6 @@
   and thus eligible for lazification.
 \<close>
 
-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"
-
-
 subsection \<open>The type \<open>lazy\<close>\<close>
 
 typedef 'a lazy = "UNIV :: 'a set" ..