# HG changeset patch
# User haftmann
# Date 1281596419 -7200
# Node ID 370712dd46284860a499e43d53fbbfa8fd45f7ed
# Parent  60acf9470a9b7012b2e70d4e254da3e5e0eebb2a
tuned

diff -r 60acf9470a9b -r 370712dd4628 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Aug 12 08:58:32 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Aug 12 09:00:19 2010 +0200
@@ -541,10 +541,10 @@
         val ((v, ty), t) = dest_abs (t2, ty2);
       in ICase (((force t1, ty), [(IVar v, tr_bind' t)]), dummy_case_term) end
     and tr_bind' t = case unfold_app t
-         of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bind c
-              then tr_bind'' [(x1, ty1), (x2, ty2)]
-              else force t
-          | _ => force t;
+     of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bind c
+          then tr_bind'' [(x1, ty1), (x2, ty2)]
+          else force t
+      | _ => force t;
     fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase (((IVar (SOME dummy_name), unitT),
       [(unitt, tr_bind'' ts)]), dummy_case_term)
     fun imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys)