src/HOL/Isar_examples/Hoare.thy
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);