src/HOL/Codatatype/Tools/bnf_lfp.ML

 
 open BNF_Def
 open BNF_Util
 open BNF_Tactics
 open BNF_FP_Util
+open BNF_FP_Sugar
 open BNF_LFP_Util
 open BNF_LFP_Tactics
 
 (*all bnfs have the same lives*)
 fun bnf_lfp mixfixes resBs bs (resDs, Dss) bnfs lthy =

           |> Thm.close_derivation;
       in
         `split_conj_thm unique_mor
       end;
 
-    val (iter_unique_thms, iter_unique_thm) =
-      `split_conj_thm (mk_conjIN n RS
+    val iter_unique_thms =
+      split_conj_thm (mk_conjIN n RS
         (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS iter_unique_mor_thm))
 
     val iter_fld_thms =
       map (fn thm => (mor_incl_thm OF replicate n @{thm subset_UNIV}) RS thm RS sym)
         iter_unique_mor_thms;

           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
             bs thmss)
       in
-        lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd
+        timer; lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd
       end;
 
       val common_notes =
         [(fld_inductN, [fld_induct_thm]),
         (fld_induct2N, [fld_induct2_thm])]

     ((unfs, flds, iters, recs, unf_fld_thms, fld_unf_thms, fld_inject_thms, iter_thms, rec_thms),
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "data_raw"} "least fixed points of BNF equations"
+  Outer_Syntax.local_theory @{command_spec "data_raw"}
+    "define BNF-based inductive datatypes (low-level)"
     (Parse.and_list1
       ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >>
       (snd oo fp_bnf_cmd bnf_lfp o apsnd split_list o split_list));
 
+val _ =
+  Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes"
+    (parse_datatype_cmd true bnf_lfp);
+
 end;