# 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