src/HOL/Tools/hologic.ML

   val mk_message_string: string -> term
   val dest_message_string: term -> string
   val mk_typerep: typ -> term
   val mk_term_of: typ -> term -> term
   val reflect_term: term -> term
+  val mk_return: typ -> typ -> term -> term
+  val mk_ST: ((term * typ) * (string * typ) option)  list -> term -> typ -> typ option * typ -> term
 end;
 
 structure HOLogic: HOLOGIC =
 struct
 

       Const ("Code_Eval.Const", message_stringT --> typerepT --> termT)
         $ mk_message_string c $ mk_typerep T
   | reflect_term (t1 $ t2) =
       Const ("Code_Eval.App", termT --> termT --> termT)
         $ reflect_term t1 $ reflect_term t2
-  | reflect_term (t as Free _) = t
-  | reflect_term (t as Bound _) = t
-  | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t);
+  | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t)
+  | reflect_term t = t;
+
+
+(* open state monads *)
+
+fun mk_return T U x = pair_const T U $ x;
+
+fun mk_ST clauses t U (someT, V) =
+  let
+    val R = case someT of SOME T => mk_prodT (T, V) | NONE => V
+    fun mk_clause ((t, U), SOME (v, T)) (t', U') =
+          (Const ("Product_Type.scomp", (U --> mk_prodT (T, U')) --> (T --> U' --> R) --> U --> R)
+            $ t $ lambda (Free (v, T)) t', U)
+      | mk_clause ((t, U), NONE) (t', U') =
+          (Const ("Product_Type.fcomp", (U --> U') --> (U' --> R) --> U --> R)
+            $ t $ t', U)
+  in fold_rev mk_clause clauses (t, U) |> fst end;
 
 end;