| changeset 5706 | 21706a735c8d |
| parent 5701 | e57980ec351b |
| child 6012 | 1894bfc4aee9 |
--- a/src/HOL/UNITY/Handshake.ML Wed Oct 21 13:01:17 1998 +0200 +++ b/src/HOL/UNITY/Handshake.ML Wed Oct 21 13:29:01 1998 +0200 @@ -9,7 +9,7 @@ *) (*split_all_tac causes a big blow-up*) -claset_ref() := claset() delSWrapper "record_split_tac"; +claset_ref() := claset() delSWrapper record_split_name; Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init]; program_defs_ref := [F_def, G_def];