# HG changeset patch # User haftmann # Date 1241690535 -7200 # Node ID 9f151b0965333bcd828ec480791f66ef5a2fd827 # Parent 0954ed96e2d5de711b94d9c917eb6d440e7339e5 explicit type arguments in constants diff -r 0954ed96e2d5 -r 9f151b096533 src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed May 06 19:42:27 2009 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu May 07 12:02:15 2009 +0200 @@ -317,7 +317,7 @@ val dummy_type = ITyVar dummy_name; val dummy_case_term = IVar dummy_name; (*assumption: dummy values are not relevant for serialization*) - val unitt = IConst (unit', ([], [])); + val unitt = IConst (unit', (([], []), [])); fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t) | dest_abs (t, ty) = let @@ -353,10 +353,10 @@ | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase (((imp_monad_bind bind' return' unit' t, ty), (map o pairself) (imp_monad_bind bind' return' unit') pats), imp_monad_bind bind' return' unit' t0); - fun imp_program naming = (Graph.map_nodes o map_terms_stmt) - (imp_monad_bind (lookup naming @{const_name bindM}) - (lookup naming @{const_name return}) - (lookup naming @{const_name Unity})); + fun imp_program naming = (Graph.map_nodes o map_terms_stmt) + (imp_monad_bind (lookup naming @{const_name bindM}) + (lookup naming @{const_name return}) + (lookup naming @{const_name Unity})); in