src/HOL/Tools/datatype_codegen.ML

--- a/src/HOL/Tools/datatype_codegen.ML	Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Wed Mar 04 10:45:52 2009 +0100
@@ -6,8 +6,8 @@
 
 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;
 
@@ -85,7 +85,7 @@
             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,
@@ -216,8 +216,8 @@
       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)
@@ -323,7 +323,7 @@
 
 (* 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;
@@ -357,10 +357,13 @@
 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;
 
@@ -369,10 +372,10 @@
 
 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
@@ -397,7 +400,7 @@
 
 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 =
@@ -445,7 +448,7 @@
       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}])
@@ -460,10 +463,10 @@
               ([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