# HG changeset patch
# User blanchet
# Date 1348101768 -7200
# Node ID 24029cbec12aafdd9de96f8461f65e6ccfb64642
# Parent  ffc06b54cb223f6060fdee982996d668b6088432
tuned ID/DEADID setup

diff -r ffc06b54cb22 -r 24029cbec12a src/HOL/Codatatype/Basic_BNFs.thy
--- a/src/HOL/Codatatype/Basic_BNFs.thy	Wed Sep 19 21:07:09 2012 +0200
+++ b/src/HOL/Codatatype/Basic_BNFs.thy	Thu Sep 20 02:42:48 2012 +0200
@@ -73,29 +73,6 @@
 lemma DEADID_pred[simp]: "DEADID_pred = (op =)"
 unfolding DEADID_pred_def DEADID.rel_Id by simp
 
-ML {*
-signature BASIC_BNFS =
-sig
-  val ID_bnf: BNF_Def.BNF
-  val ID_rel_def: thm
-  val ID_pred_def: thm
-
-  val DEADID_bnf: BNF_Def.BNF
-end;
-
-structure Basic_BNFs : BASIC_BNFS =
-struct
-
-val ID_bnf = the (BNF_Def.bnf_of @{context} "Basic_BNFs.ID");
-val DEADID_bnf = the (BNF_Def.bnf_of @{context} "Basic_BNFs.DEADID");
-
-val rel_def = BNF_Def.rel_def_of_bnf ID_bnf;
-val ID_rel_def = rel_def RS sym;
-val ID_pred_def = Local_Defs.unfold @{context} [rel_def] (BNF_Def.pred_def_of_bnf ID_bnf) RS sym;
-
-end;
-*}
-
 definition sum_setl :: "'a + 'b \<Rightarrow> 'a set" where
 "sum_setl x = (case x of Inl z => {z} | _ => {})"
 
diff -r ffc06b54cb22 -r 24029cbec12a src/HOL/Codatatype/Tools/bnf_comp.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Wed Sep 19 21:07:09 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -704,9 +704,16 @@
     ((bnf', deads), lthy' |> Local_Theory.notes notes |> snd)
   end;
 
+val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID");
+val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID");
+
+val ID_rel_def = rel_def_of_bnf ID_bnf;
+val ID_rel_def' = ID_rel_def RS sym;
+val ID_pred_def' = Local_Defs.unfold @{context} [ID_rel_def] (pred_def_of_bnf ID_bnf) RS sym;
+
 fun bnf_of_typ _ _ _ (T as TFree _) (unfold, lthy) =
-    ((Basic_BNFs.ID_bnf, ([], [T])), (add_to_unfold_opt NONE NONE
-      (SOME Basic_BNFs.ID_rel_def) (SOME Basic_BNFs.ID_pred_def) unfold, lthy))
+    ((ID_bnf, ([], [T])),
+      (add_to_unfold_opt NONE NONE (SOME ID_rel_def') (SOME ID_pred_def') unfold, lthy))
   | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
   | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
     let
@@ -714,7 +721,7 @@
       val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
     in
       (case bnf_opt of
-        NONE => ((Basic_BNFs.DEADID_bnf, ([T], [])), (unfold, lthy))
+        NONE => ((DEADID_bnf, ([T], [])), (unfold, lthy))
       | SOME bnf =>
         if forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then
           let
diff -r ffc06b54cb22 -r 24029cbec12a src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 19 21:07:09 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -663,6 +663,8 @@
         val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
         fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
 
+        (* TODO: Also note "recs", "simps", and "splits" if "nn > 1" (for compatibility with the
+           old package)? *)
         val common_notes =
           (if nn > 1 then [(inductN, [induct_thm], [induct_case_names_attr])] else [])
           |> map (fn (thmN, thms, attrs) =>