src/HOL/Tools/datatype_rep_proofs.ML

 val f_myinv_f = thm "f_myinv_f";
 val myinv_f_f = thm "myinv_f_f";
 
 
 fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
-  #exhaustion (valOf (Symtab.lookup (dt_info, tname)));
+  #exhaustion (the (Symtab.curried_lookup dt_info tname));
 
 (******************************************************************************)
 
 fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
       new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =

 
     fun make_iso_defs (ds, (thy, char_thms)) =
       let
         val ks = map fst ds;
         val (_, (tname, _, _)) = hd ds;
-        val {rec_rewrites, rec_names, ...} = valOf (Symtab.lookup (dt_info, tname));
+        val {rec_rewrites, rec_names, ...} = the (Symtab.curried_lookup dt_info tname);
 
         fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) =
           let
             val (fs', eqns', _) = Library.foldl (make_iso_def k ks (length constrs))
               ((fs, eqns, 1), constrs);

     (* prove  inj dt_Rep_i  and  dt_Rep_i x : dt_rep_set_i *)
 
     fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
       let
         val (_, (tname, _, _)) = hd ds;
-        val {induction, ...} = valOf (Symtab.lookup (dt_info, tname));
+        val {induction, ...} = the (Symtab.curried_lookup dt_info tname);
 
         fun mk_ind_concl (i, _) =
           let
             val T = List.nth (recTs, i);
             val Rep_t = Const (List.nth (all_rep_names, i), T --> Univ_elT);