| changeset 30235 | 58d147683393 |
| parent 16417 | 9bc16273c2d4 |
| child 32960 | 69916a850301 |
--- a/src/HOL/NanoJava/State.thy Tue Mar 03 17:05:18 2009 +0100 +++ b/src/HOL/NanoJava/State.thy Wed Mar 04 10:47:20 2009 +0100 @@ -33,7 +33,7 @@ constdefs init_vars:: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" - "init_vars m == option_map (\<lambda>T. Null) o m" + "init_vars m == Option.map (\<lambda>T. Null) o m" text {* private: *} types heap = "loc \<rightharpoonup> obj"