--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Nov 26 20:05:34 2014 +0100
@@ -691,7 +691,7 @@
| imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
| imp_monad_bind (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) =
ICase { term = imp_monad_bind t, typ = ty,
- clauses = (map o pairself) imp_monad_bind clauses, primitive = imp_monad_bind t0 };
+ clauses = (map o apply2) imp_monad_bind clauses, primitive = imp_monad_bind t0 };
in (Code_Symbol.Graph.map o K o map_terms_stmt) imp_monad_bind end;