src/HOL/Tools/datatype_rep_proofs.ML

--- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Sep 05 17:38:17 2005 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Sep 05 17:38:18 2005 +0200
@@ -35,7 +35,7 @@
 
 
 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));
 
 (******************************************************************************)
 
@@ -356,7 +356,7 @@
       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
@@ -412,7 +412,7 @@
     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