| changeset 5706 | 21706a735c8d |
| parent 5701 | e57980ec351b |
| child 5804 | 8e0a4c4fd67b |
--- a/src/HOL/UNITY/Comp.ML Wed Oct 21 13:01:17 1998 +0200 +++ b/src/HOL/UNITY/Comp.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; Delsimps [split_paired_All];