src/HOL/thy_syntax.ML
changeset 4204 7b15e7eee982
parent 4184 23a09f2fd687
child 4225 3d9e551bc5a6
     1.1 --- a/src/HOL/thy_syntax.ML	Wed Nov 12 12:23:37 1997 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Wed Nov 12 12:24:55 1997 +0100
     1.3 @@ -165,7 +165,7 @@
     1.4      \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
     1.5        ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
     1.6      \            ALLGOALS Asm_simp_tac]);\n\
     1.7 -    \val split_"^tname^"_case_prem = prove_goal thy (#2(split_"^tname^"_eqns))\n\
     1.8 +    \val split_"^tname^"_case_asm = prove_goal thy (#2(split_"^tname^"_eqns))\n\
     1.9      \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
    1.10        ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
    1.11      \            ALLGOALS Asm_simp_tac]);\n\