changeset 32808 | 0059238fe4bc |
parent 32799 | 7478ea535416 |
child 32809 | e72347dd3e64 |
--- a/src/HOL/Tools/record.ML Thu Oct 01 11:33:32 2009 +0200 +++ b/src/HOL/Tools/record.ML Thu Oct 01 12:15:35 2009 +0200 @@ -1052,7 +1052,6 @@ then noopt () else opt (); -(* FIXME non-standard name for partial identity; rename to check_... (??) *) fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) = (case get_updates thy u of SOME u_name => u_name = s