# HG changeset patch
# User Andreas Lochbihler
# Date 1442348706 -7200
# Node ID e4716b792713b63cf87746ed6cac192c6dc6c499
# Parent  16775cad1a5c8ed025f48c62037f8f473e560ace
avoid module dependency cycles

diff -r 16775cad1a5c -r e4716b792713 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Sep 15 17:09:13 2015 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Sep 15 22:25:06 2015 +0200
@@ -224,6 +224,18 @@
 code_pred List.member
   by(auto simp add: List.member_def elim: list.set_cases)
 
+code_identifier constant member_i_i
+   \<rightharpoonup> (SML) "List.member_i_i"
+  and (OCaml) "List.member_i_i"
+  and (Haskell) "List.member_i_i"
+  and (Scala) "List.member_i_i"
+
+code_identifier constant member_i_o
+   \<rightharpoonup> (SML) "List.member_i_o"
+  and (OCaml) "List.member_i_o"
+  and (Haskell) "List.member_i_o"
+  and (Scala) "List.member_i_o"
+
 section \<open>Setup for String.literal\<close>
 
 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name "STR"}]\<close>