| changeset 55466 | 786edc984c98 |
| parent 42463 | f270e3e18be5 |
| child 58249 | 180f1b3508ed |
--- a/src/HOL/NanoJava/State.thy Fri Feb 14 07:53:45 2014 +0100 +++ b/src/HOL/NanoJava/State.thy Fri Feb 14 07:53:46 2014 +0100 @@ -28,7 +28,7 @@ (type) "obj" \<leftharpoondown> (type) "cname \<times> fields" definition init_vars :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" where - "init_vars m == Option.map (\<lambda>T. Null) o m" + "init_vars m == map_option (\<lambda>T. Null) o m" text {* private: *} type_synonym heap = "loc \<rightharpoonup> obj"