src/HOL/Tools/Datatype/datatype_realizer.ML

-(*  Title:      HOL/Tools/datatype_realizer.ML
+(*  Title:      HOL/Tools/Datatype/datatype_realizer.ML
     Author:     Stefan Berghofer, TU Muenchen
 
-Porgram extraction from proofs involving datatypes:
-Realizers for induction and case analysis
+Program extraction from proofs involving datatypes:
+realizers for induction and case analysis.
 *)
 
 signature DATATYPE_REALIZER =
 sig
   val add_dt_realizers: Datatype.config -> string list -> theory -> theory
   val setup: theory -> theory
 end;
 
-structure DatatypeRealizer : DATATYPE_REALIZER =
+structure Datatype_Realizer : DATATYPE_REALIZER =
 struct
 
-open DatatypeAux;
+open Datatype_Aux;
 
 fun subsets i j = if i <= j then
        let val is = subsets (i+1) j
        in map (fn ks => i::ks) is @ is end
      else [[]];

 
     val (prems, rec_fns) = split_list (flat (fst (fold_map
       (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
         let
           val Ts = map (typ_of_dtyp descr sorts) cargs;
-          val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
+          val tnames = Name.variant_list pnames (Datatype_Prop.make_tnames Ts);
           val recs = filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
           val frees = tnames ~~ Ts;
 
           fun mk_prems vs [] = 
                 let

     fun mk_proj j [] t = t
       | mk_proj j (i :: is) t = if null is then t else
           if (j: int) = i then HOLogic.mk_fst t
           else mk_proj j is (HOLogic.mk_snd t);
 
-    val tnames = DatatypeProp.make_tnames recTs;
+    val tnames = Datatype_Prop.make_tnames recTs;
     val fTs = map fastype_of rec_fns;
     val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T
       (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0)))
         (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names);
     val r = if null is then Extraction.nullt else

       |> Sign.root_path
       |> PureThy.store_thm
         (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
       ||> Sign.restore_naming thy;
 
-    val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
+    val ivs = rev (Term.add_vars (Logic.varify (Datatype_Prop.make_ind [descr] sorts)) []);
     val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
     val ivs1 = map Var (filter_out (fn (_, T) =>
       tname_of (body_type T) mem ["set", "bool"]) ivs);
     val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
 

     val rT' = TVar (("'P", 0), HOLogic.typeS);
 
     fun make_casedist_prem T (cname, cargs) =
       let
         val Ts = map (typ_of_dtyp descr sorts) cargs;
-        val frees = Name.variant_list ["P", "y"] (DatatypeProp.make_tnames Ts) ~~ Ts;
+        val frees = Name.variant_list ["P", "y"] (Datatype_Prop.make_tnames Ts) ~~ Ts;
         val free_ts = map Free frees;
         val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
       in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
         (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
           HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $