# HG changeset patch
# User wenzelm
# Date 1470154404 -7200
# Node ID 161c5d8ae266d2ac472cad157ad1993edaccfd46
# Parent  a1bdc546f27695243cd18ef1e4e8015cb7438ae5
avoid confusion with 'case' and "cases";

diff -r a1bdc546f276 -r 161c5d8ae266 src/HOL/Library/Simps_Case_Conv.thy
--- a/src/HOL/Library/Simps_Case_Conv.thy	Tue Aug 02 18:11:17 2016 +0200
+++ b/src/HOL/Library/Simps_Case_Conv.thy	Tue Aug 02 18:13:24 2016 +0200
@@ -8,6 +8,7 @@
   "simps_of_case" "case_of_simps" :: thy_decl
 abbrevs
   "simps_of_case" = ""
+  "case_of_simps" = ""
 begin
 
 ML_file "simps_case_conv.ML"