# HG changeset patch
# User oheimb
# Date 879333895 -3600
# Node ID 7b15e7eee9823fed2a44bc5ae5e700f405eb9de8
# Parent  ca73de799b73ead4452005c4e68a5b962b3eb63c
renamed split_T_case_prem to split_T_case_asm

diff -r ca73de799b73 -r 7b15e7eee982 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Wed Nov 12 12:23:37 1997 +0100
+++ b/src/HOL/thy_syntax.ML	Wed Nov 12 12:24:55 1997 +0100
@@ -165,7 +165,7 @@
     \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
       ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
     \            ALLGOALS Asm_simp_tac]);\n\
-    \val split_"^tname^"_case_prem = prove_goal thy (#2(split_"^tname^"_eqns))\n\
+    \val split_"^tname^"_case_asm = prove_goal thy (#2(split_"^tname^"_eqns))\n\
     \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
       ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
     \            ALLGOALS Asm_simp_tac]);\n\