src/HOL/thy_syntax.ML
changeset 4184 23a09f2fd687
parent 4106 01fa6e7e7196
child 4204 7b15e7eee982
     1.1 --- a/src/HOL/thy_syntax.ML	Thu Nov 06 16:44:35 1997 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Fri Nov 07 08:25:02 1997 +0100
     1.3 @@ -123,7 +123,7 @@
     1.4  
     1.5    (*generate string for calling add_datatype and build_record*)
     1.6    fun mk_params ((ts, tname), cons) =
     1.7 -    "val (thy,"^tname^"_add_primrec,size_"^tname^"_eqns,split_"^tname^"_eqn) =\n\
     1.8 +    "val (thy,"^tname^"_add_primrec,size_"^tname^"_eqns,split_"^tname^"_eqns) =\n\
     1.9      \    Datatype.add_datatype\n"
    1.10      ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
    1.11      \val thy = ("^tname^"_add_primrec size_"^tname^"_eqns thy)\n\
    1.12 @@ -161,7 +161,11 @@
    1.13      \val dummy = Addsimps(map (fn (_,eqn) =>\n\
    1.14      \ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
    1.15                       "] eqn (fn _ => [Simp_tac 1])) size_"^tname^"_eqns);\n\
    1.16 -    \val split_"^tname^"_case = prove_goal thy split_"^tname^"_eqn\n\
    1.17 +    \val split_"^tname^"_case = prove_goal thy (#1(split_"^tname^"_eqns))\n\
    1.18 +    \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
    1.19 +      ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
    1.20 +    \            ALLGOALS Asm_simp_tac]);\n\
    1.21 +    \val split_"^tname^"_case_prem = prove_goal thy (#2(split_"^tname^"_eqns))\n\
    1.22      \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
    1.23        ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
    1.24      \            ALLGOALS Asm_simp_tac]);\n\