src/HOL/Tools/datatype_rep_proofs.ML
changeset 17261 193b84a70ca4
parent 16486 1a12cdb6ee6b
child 17412 e26cb20ef0cc
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Sep 05 17:38:17 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Sep 05 17:38:18 2005 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  
     1.5  
     1.6  fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
     1.7 -  #exhaustion (valOf (Symtab.lookup (dt_info, tname)));
     1.8 +  #exhaustion (the (Symtab.curried_lookup dt_info tname));
     1.9  
    1.10  (******************************************************************************)
    1.11  
    1.12 @@ -356,7 +356,7 @@
    1.13        let
    1.14          val ks = map fst ds;
    1.15          val (_, (tname, _, _)) = hd ds;
    1.16 -        val {rec_rewrites, rec_names, ...} = valOf (Symtab.lookup (dt_info, tname));
    1.17 +        val {rec_rewrites, rec_names, ...} = the (Symtab.curried_lookup dt_info tname);
    1.18  
    1.19          fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) =
    1.20            let
    1.21 @@ -412,7 +412,7 @@
    1.22      fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
    1.23        let
    1.24          val (_, (tname, _, _)) = hd ds;
    1.25 -        val {induction, ...} = valOf (Symtab.lookup (dt_info, tname));
    1.26 +        val {induction, ...} = the (Symtab.curried_lookup dt_info tname);
    1.27  
    1.28          fun mk_ind_concl (i, _) =
    1.29            let