src/HOL/Tools/datatype_codegen.ML

 Code generator facilities for inductive datatypes.
 *)
 
 signature DATATYPE_CODEGEN =
 sig
-  val get_eq: theory -> string -> thm list
-  val get_case_cert: theory -> string -> thm
+  val mk_eq: theory -> string -> thm list
+  val mk_case_cert: theory -> string -> thm
   val setup: theory -> theory
 end;
 
 structure DatatypeCodegen : DATATYPE_CODEGEN =
 struct

           let
             val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs;
             val dts' = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
             val T = Type (tname, dts');
             val rest = mk_term_of_def gr "and " xs;
-            val (_, eqs) = foldl_map (fn (prfx, (cname, Ts)) =>
+            val (_, eqs) = Library.foldl_map (fn (prfx, (cname, Ts)) =>
               let val args = map (fn i =>
                 str ("x" ^ string_of_int i)) (1 upto length Ts)
               in ("  | ", Pretty.blk (4,
                 [str prfx, mk_term_of gr module' false T, Pretty.brk 1,
                  if null Ts then str (snd (get_const_id gr cname))

        invoke_codegen thy defs dep module brack (eta_expand c ts (i+1)) gr
     else
       let
         val ts1 = Library.take (i, ts);
         val t :: ts2 = Library.drop (i, ts);
-        val names = foldr OldTerm.add_term_names
-          (map (fst o fst o dest_Var) (foldr OldTerm.add_term_vars [] ts1)) ts1;
+        val names = List.foldr OldTerm.add_term_names
+          (map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1;
         val (Ts, dT) = split_last (Library.take (i+1, fst (strip_type T)));
 
         fun pcase [] [] [] gr = ([], gr)
           | pcase ((cname, cargs)::cs) (t::ts) (U::Us) gr =
               let

   end;
 
 
 (* case certificates *)
 
-fun get_case_cert thy tyco =
+fun mk_case_cert thy tyco =
   let
     val raw_thms =
       (#case_rewrites o DatatypePackage.the_datatype thy) tyco;
     val thms as hd_thm :: _ = raw_thms
       |> Conjunction.intr_balanced

   end;
 
 fun add_datatype_cases dtco thy =
   let
     val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco;
-    val certs = get_case_cert thy dtco;
+    val cert = mk_case_cert thy dtco;
+    fun add_case_liberal thy = thy
+      |> try (Code.add_case cert)
+      |> the_default thy;
   in
     thy
-    |> Code.add_case certs
+    |> add_case_liberal
     |> fold_rev Code.add_default_eqn case_rewrites
   end;
 
 
 (* equality *)
 
 local
 
-val not_sym = thm "HOL.not_sym";
-val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
-val refl = thm "refl";
-val eqTrueI = thm "eqTrueI";
+val not_sym = @{thm HOL.not_sym};
+val not_false_true = iffD2 OF [nth @{thms HOL.simp_thms} 7, TrueI];
+val refl = @{thm refl};
+val eqTrueI = @{thm eqTrueI};
 
 fun mk_distinct cos =
   let
     fun sym_product [] = []
       | sym_product (x::xs) = map (pair x) xs @ sym_product xs;

       in HOLogic.mk_Trueprop t end;
   in map mk_dist (sym_product cos) end;
 
 in
 
-fun get_eq thy dtco =
+fun mk_eq thy dtco =
   let
     val (vs, cs) = DatatypePackage.the_datatype_spec thy dtco;
     fun mk_triv_inject co =
       let
         val ct' = Thm.cterm_of thy

         val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
         val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
       in (thm', lthy') end;
     fun tac thms = Class.intro_classes_tac []
       THEN ALLGOALS (ProofContext.fact_tac thms);
-    fun get_eq' thy dtco = get_eq thy dtco
+    fun mk_eq' thy dtco = mk_eq thy dtco
       |> map (Code_Unit.constrain_thm thy [HOLogic.class_eq])
       |> map Simpdata.mk_eq
       |> map (MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}])
       |> map (AxClass.unoverload thy);
     fun add_eq_thms dtco thy =

         val eq_refl = @{thm HOL.eq_refl}
           |> Thm.instantiate
               ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], [])
           |> Simpdata.mk_eq
           |> AxClass.unoverload thy;
-        fun get_thms () = (eq_refl, false)
-          :: rev (map (rpair true) (get_eq' (Theory.deref thy_ref) dtco));
+        fun mk_thms () = (eq_refl, false)
+          :: rev (map (rpair true) (mk_eq' (Theory.deref thy_ref) dtco));
       in
-        Code.add_eqnl (const, Lazy.lazy get_thms) thy
+        Code.add_eqnl (const, Lazy.lazy mk_thms) thy
       end;
   in
     thy
     |> TheoryTarget.instantiation (dtcos, vs', [HOLogic.class_eq])
     |> fold_map add_def dtcos