diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy
index d763880..853ec99 100644
--- a/Isabelle_DOF/thys/Isa_DOF.thy
+++ b/Isabelle_DOF/thys/Isa_DOF.thy
@@ -1866,7 +1866,7 @@ fun check_invariants thy binding =
 fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} binding cid_pos doc_attrs thy =
   let
     val oid = Binding.name_of binding
-    val (((name, args_cid), typ), pos') = check_classref is_monitor cid_pos thy
+    val (((name, args_cid), typ:typ), pos') = check_classref is_monitor cid_pos thy
     val cid_pos' = (name, pos')
     val cid_long = fst cid_pos'
     val default_cid = args_cid = DOF_core.default_cid
@@ -1891,13 +1891,13 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} bi
                             val defaults_init = create_default_object thy binding cid_long typ
                             fun conv (na, _(*ty*), parsed_term) =(Binding.name_of na, Binding.pos_of na, "=", parsed_term);
                             val S = map conv (DOF_core.get_attribute_defaults cid_long thy);
-                            val (defaults, _(*ty*), _) = calc_update_term {mk_elaboration=false}
+                            val (defaults, _) = calc_update_term {mk_elaboration=false}
                                                                       thy (name, typ) S defaults_init;
-                            val (value_term', _(*ty*), _) = calc_update_term {mk_elaboration=true}
+                            val (value_term', _) = calc_update_term {mk_elaboration=true}
                                                                       thy (name, typ) assns' defaults
                           in if Config.get_global thy DOF_core.object_value_debug
                              then let
-                                    val (input_term, _(*ty*), _) = calc_update_term {mk_elaboration=false}
+                                    val (input_term, _) = calc_update_term {mk_elaboration=false}
                                                                         thy (name, typ)  assns' defaults
                                   in (input_term, value_term') end
                              else (\<^term>\<open>()\<close>, value_term') end