--- 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\