src/HOL/Tools/Datatype/datatype.ML

--- a/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 29 16:09:16 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Oct 29 16:09:41 2009 +0100
@@ -96,6 +96,7 @@
      cases = cases |> fold Symtab.update
        (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)});
 
+
 (* complex queries *)
 
 fun the_spec thy dtco =
@@ -157,6 +158,7 @@
     | NONE => NONE;
 
 
+
 (** various auxiliary **)
 
 (* prepare datatype specifications *)
@@ -209,6 +211,7 @@
 
 end;
 
+
 (* translation rules for case *)
 
 fun make_case ctxt = DatatypeCase.make_case
@@ -230,6 +233,7 @@
     [], []);
 
 
+
 (** document antiquotation **)
 
 val _ = ThyOutput.antiquotation "datatype" Args.tyname
@@ -256,15 +260,17 @@
     in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
 
 
+
 (** abstract theory extensions relative to a datatype characterisation **)
 
-structure DatatypeInterpretation = InterpretationFun
+structure Datatype_Interpretation = InterpretationFun
   (type T = config * string list val eq: T * T -> bool = eq_snd op =);
-fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
+fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
 
 fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
     (index, (((((((((((_, (tname, _, _))), inject), distinct),
-      exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong), (split, split_asm))) =
+      exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong),
+        (split, split_asm))) =
   (tname,
    {index = index,
     alt_names = alt_names,
@@ -311,7 +317,8 @@
       config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
 
     val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
-    val dt_infos = map_index (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
+    val dt_infos = map_index
+      (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
       (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
         case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
     val dt_names = map fst dt_infos;
@@ -339,14 +346,16 @@
     |> snd
     |> add_case_tr' case_names
     |> register dt_infos
-    |> DatatypeInterpretation.data (config, dt_names)
+    |> Datatype_Interpretation.data (config, dt_names)
     |> pair dt_names
   end;
 
 
+
 (** declare existing type as datatype **)
 
-fun prove_rep_datatype config dt_names alt_names descr sorts raw_inject half_distinct raw_induct thy1 =
+fun prove_rep_datatype config dt_names alt_names descr sorts
+    raw_inject half_distinct raw_induct thy1 =
   let
     val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
     val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
@@ -419,7 +428,8 @@
             (*FIXME somehow dubious*)
       in
         ProofContext.theory_result
-          (prove_rep_datatype config dt_names alt_names descr vs raw_inject half_distinct raw_induct)
+          (prove_rep_datatype config dt_names alt_names descr vs
+            raw_inject half_distinct raw_induct)
         #-> after_qed
       end;
   in
@@ -432,6 +442,7 @@
 val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
 
 
+
 (** definitional introduction of datatypes **)
 
 fun gen_add_datatype prep_typ config new_type_names dts thy =
@@ -447,16 +458,20 @@
     val (tyvars, _, _, _)::_ = dts;
     val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
       let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
-      in (case duplicates (op =) tvs of
-            [] => if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
-                  else error ("Mutually recursive datatypes must have same type parameters")
-          | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
-              " : " ^ commas dups))
+      in
+        (case duplicates (op =) tvs of
+          [] =>
+            if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
+            else error ("Mutually recursive datatypes must have same type parameters")
+        | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
+            " : " ^ commas dups))
       end) dts);
     val dt_names = map fst new_dts;
 
-    val _ = (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
-      [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
+    val _ =
+      (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
+        [] => ()
+      | dups => error ("Duplicate datatypes: " ^ commas dups));
 
     fun prep_dt_spec ((tvs, tname, mx, constrs), tname') (dts', constr_syntax, sorts, i) =
       let
@@ -510,13 +525,15 @@
 val datatype_cmd = snd ooo gen_add_datatype read_typ default_config;
 
 
+
 (** package setup **)
 
 (* setup theory *)
 
 val setup =
   trfun_setup #>
-  DatatypeInterpretation.init;
+  Datatype_Interpretation.init;
+
 
 (* outer syntax *)