# HG changeset patch
# User blanchet
# Date 1410294314 -7200
# Node ID 10105897bc221085c6ce3f8165be9a0783496f0f
# Parent  a15731cf1835cb4b9e0248be9df66e422d091635
restored old case names

diff -r a15731cf1835 -r 10105897bc22 src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Bali/AxCompl.thy	Tue Sep 09 22:25:14 2014 +0200
@@ -1318,7 +1318,7 @@
       show "G,A\<turnstile>{=:n} \<langle>Init C\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
         by (rule MGFn_Init)
     next
-      case Nil
+      case Nil_expr
       show "G,A\<turnstile>{=:n} \<langle>[]\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
         apply -
         apply (rule MGFn_NormalI)
@@ -1326,7 +1326,7 @@
         apply (fastforce intro: eval.Nil)
         done
     next
-      case (Cons e es)
+      case (Cons_expr e es)
       thus "G,A\<turnstile>{=:n} \<langle>e# es\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
         apply -
         apply (rule MGFn_NormalI)