--- 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