changeset 31723 | f5cafe803b55 |
parent 30549 | d2d7874648bd |
child 31758 | 3edd5f813f01 |
--- a/src/HOL/Isar_examples/Hoare.thy Thu Jun 18 18:31:14 2009 -0700 +++ b/src/HOL/Isar_examples/Hoare.thy Fri Jun 19 17:23:21 2009 +0200 @@ -260,7 +260,7 @@ | bexp_tr' _ _ = raise Match; fun upd_tr' (x_upd, T) = - (case try (unsuffix RecordPackage.updateN) x_upd of + (case try (unsuffix Record.updateN) x_upd of SOME x => (x, if T = dummyT then T else Term.domain_type T) | NONE => raise Match);