src/HOL/Nominal/nominal_datatype.ML
changeset 33035 15eab423e573
parent 32960 69916a850301
child 33040 cffdb7b28498
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Tue Oct 20 23:25:04 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Oct 21 00:36:12 2009 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4  
     1.5  fun dt_cases (descr: descr) (_, args, constrs) =
     1.6    let
     1.7 -    fun the_bname i = Long_Name.base_name (#1 (valOf (AList.lookup (op =) descr i)));
     1.8 +    fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
     1.9      val bnames = map the_bname (distinct op = (maps dt_recs args));
    1.10    in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
    1.11  
    1.12 @@ -58,7 +58,7 @@
    1.13  fun induct_cases descr =
    1.14    DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
    1.15  
    1.16 -fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
    1.17 +fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
    1.18  
    1.19  in
    1.20  
    1.21 @@ -233,7 +233,7 @@
    1.22      fun replace_types (Type ("Nominal.ABS", [T, U])) =
    1.23            Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
    1.24        | replace_types (Type (s, Ts)) =
    1.25 -          Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
    1.26 +          Type (the_default s (AList.lookup op = ps s), map replace_types Ts)
    1.27        | replace_types T = T;
    1.28  
    1.29      val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, Binding.name (tname ^ "_Rep"), NoSyn,