# HG changeset patch # User blanchet # Date 1410177781 -7200 # Node ID c1f3fa32d322b71463ec5539499986a4db8a4286 # Parent a456b2c0349102d0c778beed5170fc3f7cbf8872 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions diff -r a456b2c03491 -r c1f3fa32d322 src/HOL/BNF_Least_Fixpoint.thy --- a/src/HOL/BNF_Least_Fixpoint.thy Mon Sep 08 14:03:01 2014 +0200 +++ b/src/HOL/BNF_Least_Fixpoint.thy Mon Sep 08 14:03:01 2014 +0200 @@ -181,6 +181,50 @@ lemma ssubst_Pair_rhs: "\(r, s) \ R; s' = s\ \ (r, s') \ R" by (rule ssubst) +lemma all_mem_range1: + "(\y. y \ range f \ P y) \ (\x. P (f x)) " + by (rule equal_intr_rule) fast+ + +lemma all_mem_range2: + "(\fa y. fa \ range f \ y \ range fa \ P y) \ (\x xa. P (f x xa))" + by (rule equal_intr_rule) fast+ + +lemma all_mem_range3: + "(\fa fb y. fa \ range f \ fb \ range fa \ y \ range fb \ P y) \ (\x xa xb. P (f x xa xb))" + by (rule equal_intr_rule) fast+ + +lemma all_mem_range4: + "(\fa fb fc y. fa \ range f \ fb \ range fa \ fc \ range fb \ y \ range fc \ P y) \ + (\x xa xb xc. P (f x xa xb xc))" + by (rule equal_intr_rule) fast+ + +lemma all_mem_range5: + "(\fa fb fc fd y. fa \ range f \ fb \ range fa \ fc \ range fb \ fd \ range fc \ + y \ range fd \ P y) \ + (\x xa xb xc xd. P (f x xa xb xc xd))" + by (rule equal_intr_rule) fast+ + +lemma all_mem_range6: + "(\fa fb fc fd fe ff y. fa \ range f \ fb \ range fa \ fc \ range fb \ fd \ range fc \ + fe \ range fd \ ff \ range fe \ y \ range ff \ P y) \ + (\x xa xb xc xd xe xf. P (f x xa xb xc xd xe xf))" + by (rule equal_intr_rule) (fastforce, fast) + +lemma all_mem_range7: + "(\fa fb fc fd fe ff fg y. fa \ range f \ fb \ range fa \ fc \ range fb \ fd \ range fc \ + fe \ range fd \ ff \ range fe \ fg \ range ff \ y \ range fg \ P y) \ + (\x xa xb xc xd xe xf xg. P (f x xa xb xc xd xe xf xg))" + by (rule equal_intr_rule) (fastforce, fast) + +lemma all_mem_range8: + "(\fa fb fc fd fe ff fg fh y. fa \ range f \ fb \ range fa \ fc \ range fb \ fd \ range fc \ + fe \ range fd \ ff \ range fe \ fg \ range ff \ fh \ range fg \ y \ range fh \ P y) \ + (\x xa xb xc xd xe xf xg xh. P (f x xa xb xc xd xe xf xg xh))" + by (rule equal_intr_rule) (fastforce, fast) + +lemmas all_mem_range = all_mem_range1 all_mem_range2 all_mem_range3 all_mem_range4 all_mem_range5 + all_mem_range6 all_mem_range7 all_mem_range8 + ML_file "Tools/BNF/bnf_lfp_util.ML" ML_file "Tools/BNF/bnf_lfp_tactics.ML" ML_file "Tools/BNF/bnf_lfp.ML" diff -r a456b2c03491 -r c1f3fa32d322 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 08 14:03:01 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 08 14:03:01 2014 +0200 @@ -536,7 +536,7 @@ val phi = Proof_Context.export_morphism lthy lthy'; - val cst' = mk_co_rec thy fp fpT Cs (Morphism.term phi cst); + val cst' = mk_co_rec thy fp Cs fpT (Morphism.term phi cst); val def' = Morphism.thm phi def; in ((cst', def'), lthy') @@ -1464,7 +1464,7 @@ sel_default_eqs) lthy end; - fun derive_maps_sets_rels (ctr_sugar as {casex, case_cong, case_thms, discs, selss, ctrs, + fun derive_map_set_rel_thms (ctr_sugar as {casex, case_cong, case_thms, discs, selss, ctrs, exhaust, exhaust_discs, disc_thmss, sel_thmss, injects, distincts, distinct_discsss, ...} : ctr_sugar, lthy) = if live = 0 then @@ -1989,7 +1989,7 @@ (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_rec_res), lthy); in (wrap_ctrs - #> derive_maps_sets_rels + #> derive_map_set_rel_thms ##>> (if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps else define_corec (the corecs_args_types) mk_binding fpTs Cs abss) xtor_co_rec diff -r a456b2c03491 -r c1f3fa32d322 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Sep 08 14:03:01 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Sep 08 14:03:01 2014 +0200 @@ -227,58 +227,56 @@ val fp_absT_infos = map #absT_info fp_sugars0; - val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct, - dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) = - fp_bnf (construct_mutualized_fp fp cliques fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs - no_defs_lthy0; + val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct, + dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) = + fp_bnf (construct_mutualized_fp fp cliques fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs + no_defs_lthy0; - val fp_abs_inverses = map #abs_inverse fp_absT_infos; - val fp_type_definitions = map #type_definition fp_absT_infos; + val fp_abs_inverses = map #abs_inverse fp_absT_infos; + val fp_type_definitions = map #type_definition fp_absT_infos; - val abss = map #abs absT_infos; - val reps = map #rep absT_infos; - val absTs = map #absT absT_infos; - val repTs = map #repT absT_infos; - val abs_inverses = map #abs_inverse absT_infos; + val abss = map #abs absT_infos; + val reps = map #rep absT_infos; + val absTs = map #absT absT_infos; + val repTs = map #repT absT_infos; + val abs_inverses = map #abs_inverse absT_infos; - val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs; - val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As; + val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs; + val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As; - val ((xtor_co_recs, recs_args_types, corecs_args_types), _) = - mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy; + val ((xtor_co_recs, recs_args_types, corecs_args_types), _) = + mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy; - fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b; + fun mk_binding b pre = Binding.prefix_name (pre ^ "_") b; - val ((co_recs, co_rec_defs), lthy) = - fold_map2 (fn b => - if fp = Least_FP then - define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps - else - define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss) - fp_bs xtor_co_recs lthy - |>> split_list; + val ((co_recs, co_rec_defs), lthy) = + fold_map2 (fn b => + if fp = Least_FP then define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps + else define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss) + fp_bs xtor_co_recs lthy + |>> split_list; - val ((common_co_inducts, co_inductss', co_rec_thmss, co_rec_disc_thmss, - co_rec_sel_thmsss), fp_sugar_thms) = - if fp = Least_FP then - derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct - xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss - fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs - lthy - |> `(fn ((inducts, induct, _), (rec_thmss, _)) => - ([induct], [inducts], rec_thmss, replicate nn [], replicate nn [])) - ||> (fn info => (SOME info, NONE)) - else - derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) - xtor_co_induct dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs - ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses - (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs - (Proof_Context.export lthy no_defs_lthy) lthy - |> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _, - (corec_sel_thmsss, _)) => - (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss, - corec_disc_thmss, corec_sel_thmsss)) - ||> (fn info => (NONE, SOME info)); + val ((common_co_inducts, co_inductss', co_rec_thmss, co_rec_disc_thmss, co_rec_sel_thmsss), + fp_sugar_thms) = + if fp = Least_FP then + derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct + xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss + fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs + lthy + |> `(fn ((inducts, induct, _), (rec_thmss, _)) => + ([induct], [inducts], rec_thmss, replicate nn [], replicate nn [])) + ||> (fn info => (SOME info, NONE)) + else + derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) + xtor_co_induct dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs + ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses + (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs + (Proof_Context.export lthy no_defs_lthy) lthy + |> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _, + (corec_sel_thmsss, _)) => + (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss, + corec_disc_thmss, corec_sel_thmsss)) + ||> (fn info => (NONE, SOME info)); val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0; diff -r a456b2c03491 -r c1f3fa32d322 src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Mon Sep 08 14:03:01 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Mon Sep 08 14:03:01 2014 +0200 @@ -37,7 +37,7 @@ val mk_compN: int -> typ list -> term * term -> term val mk_comp: typ list -> term * term -> term - val mk_co_rec: theory -> fp_kind -> typ -> typ list -> term -> term + val mk_co_rec: theory -> fp_kind -> typ list -> typ -> term -> term val mk_conjunctN: int -> int -> thm val conj_dests: int -> thm -> thm list @@ -105,7 +105,7 @@ val mk_comp = mk_compN 1; -fun mk_co_rec thy fp fpT Cs t = +fun mk_co_rec thy fp Cs fpT t = let val ((f_Cs, prebody), body) = strip_type (fastype_of t) |>> split_last; val fpT0 = case_fp fp prebody body; diff -r a456b2c03491 -r c1f3fa32d322 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Sep 08 14:03:01 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Sep 08 14:03:01 2014 +0200 @@ -462,7 +462,7 @@ fun mk_spec ({T, ctr_sugar as {exhaust_discs, sel_defs, ...}, co_rec = corec, co_rec_thms = corec_thms, co_rec_discs = corec_discs, co_rec_selss = corec_selss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss = - {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, exhaust_discs = exhaust_discs, + {corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec, exhaust_discs = exhaust_discs, sel_defs = sel_defs, fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs, fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs, diff -r a456b2c03491 -r c1f3fa32d322 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 08 14:03:01 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 08 14:03:01 2014 +0200 @@ -43,15 +43,152 @@ open Ctr_Sugar open BNF_Util +open BNF_Tactics open BNF_FP_Util open BNF_FP_Def_Sugar open BNF_FP_N2M_Sugar open BNF_LFP -val compatN = "compat_"; +val compat_N = "compat_"; +val rec_fun_N = "rec_fun_"; datatype nesting_preference = Keep_Nesting | Unfold_Nesting; +fun mk_fun_rec_rhs ctxt fpTs Cs (recs as rec1 :: _) = + let + fun repair_rec_arg_args [] [] = [] + | repair_rec_arg_args ((g_T as Type (@{type_name fun}, _)) :: g_Ts) (g :: gs) = + let + val (x_Ts, body_T) = strip_type g_T; + in + (case try HOLogic.dest_prodT body_T of + NONE => [g] + | SOME (fst_T, _) => + if member (op =) fpTs fst_T then + let val (xs, _) = mk_Frees "x" x_Ts ctxt in + map (fn mk_proj => fold_rev Term.lambda xs (mk_proj (Term.list_comb (g, xs)))) + [HOLogic.mk_fst, HOLogic.mk_snd] + end + else + [g]) + :: repair_rec_arg_args g_Ts gs + end + | repair_rec_arg_args (g_T :: g_Ts) (g :: gs) = + if member (op =) fpTs g_T then + let + val j = find_index (member (op =) Cs) g_Ts; + val h = nth gs j; + val g_Ts' = nth_drop j g_Ts; + val gs' = nth_drop j gs; + in + [g, h] :: repair_rec_arg_args g_Ts' gs' + end + else + [g] :: repair_rec_arg_args g_Ts gs; + + fun repair_back_rec_arg f_T f' = + let + val g_Ts = Term.binder_types f_T; + val (gs, _) = mk_Frees "g" g_Ts ctxt; + in + fold_rev Term.lambda gs (Term.list_comb (f', + flat_rec_arg_args (repair_rec_arg_args g_Ts gs))) + end; + + val f_Ts = binder_fun_types (fastype_of rec1); + val (fs', _) = mk_Frees "f" (replicate (length f_Ts) Term.dummyT) ctxt; + + fun mk_rec' recx = + fold_rev Term.lambda fs' (Term.list_comb (recx, map2 repair_back_rec_arg f_Ts fs')) + |> Syntax.check_term ctxt; + in + map mk_rec' recs + end; + +fun define_fun_recs fpTs Cs recs lthy = + let + val b_names = Name.variant_list [] (map base_name_of_typ fpTs); + + fun mk_binding b_name = + Binding.qualify true (compat_N ^ b_name) + (Binding.prefix_name rec_fun_N (Binding.name b_name)); + + val bs = map mk_binding b_names; + val rhss = mk_fun_rec_rhs lthy fpTs Cs recs; + in + fold_map3 (define_co_rec_as Least_FP Cs) fpTs bs rhss lthy + end; + +fun mk_fun_rec_thmss ctxt rec0_thmss (recs as rec1 :: _) rec_defs = + let + val f_Ts = binder_fun_types (fastype_of rec1); + val (fs, _) = mk_Frees "f" f_Ts ctxt; + val frecs = map (fn recx => Term.list_comb (recx, fs)) recs; + + fun mk_ctrs_of (Type (T_name, As)) = + map (mk_ctr As) (#ctrs (the (ctr_sugar_of ctxt T_name))); + + val fpTs = map (domain_type o body_fun_type o fastype_of) recs; + val fpTs_frecs = fpTs ~~ frecs; + val ctrss = map mk_ctrs_of fpTs; + val fss = unflat ctrss fs; + + fun mk_rec_call g n (Type (@{type_name fun}, [dom_T, ran_T])) = + Abs (Name.uu, dom_T, mk_rec_call g (n + 1) ran_T) + | mk_rec_call g n fpT = + let + val frec = the (AList.lookup (op =) fpTs_frecs fpT); + val xg = Term.list_comb (g, map Bound (n - 1 downto 0)); + in frec $ xg end; + + fun mk_rec_arg_arg g_T g = + g :: (if exists_subtype_in fpTs g_T then [mk_rec_call g 0 g_T] else []); + + fun mk_goal frec ctr f = + let + val g_Ts = binder_types (fastype_of ctr); + val (gs, _) = mk_Frees "g" g_Ts ctxt; + val gctr = Term.list_comb (ctr, gs); + val fgs = flat_rec_arg_args (map2 mk_rec_arg_arg g_Ts gs); + in + fold_rev (fold_rev Logic.all) [fs, gs] + (mk_Trueprop_eq (frec $ gctr, Term.list_comb (f, fgs))) + end; + + fun mk_goals ctrs fs frec = map2 (mk_goal frec) ctrs fs; + + val goalss = map3 mk_goals ctrss fss frecs; + + fun tac ctxt = + unfold_thms_tac ctxt (@{thms o_apply fst_conv snd_conv} @ rec_defs @ flat rec0_thmss) THEN + HEADGOAL (rtac refl); + + fun prove goal = + Goal.prove_sorry ctxt [] [] goal (tac o #context) + |> Thm.close_derivation; + in + map (map prove) goalss + end; + +fun define_fun_rec_derive_thms induct inducts recs0 rec_thmss fpTs lthy = + let + val thy = Proof_Context.theory_of lthy; + + (* imperfect: will not yield the expected theorem for functions taking a large number of + arguments *) + val repair_induct = unfold_thms lthy @{thms all_mem_range}; + + val induct' = repair_induct induct; + val inducts' = map repair_induct inducts; + + val Cs = map ((fn TVar ((s, _), S) => TFree (s, S)) o body_type o fastype_of) recs0; + val recs = map2 (mk_co_rec thy Least_FP Cs) fpTs recs0; + val ((recs', rec'_defs), lthy') = define_fun_recs fpTs Cs recs lthy |>> split_list; + val rec'_thmss = mk_fun_rec_thmss lthy' rec_thmss recs' rec'_defs; + in + ((induct', inducts', recs', rec'_thmss), lthy') + end; + fun reindex_desc desc = let val kks = map fst desc; @@ -130,10 +267,10 @@ val dest_dtyp = Old_Datatype_Aux.typ_of_dtyp descr; - val Ts = Old_Datatype_Aux.get_rec_types descr; - val nn = length Ts; + val fpTs' = Old_Datatype_Aux.get_rec_types descr; + val nn = length fpTs'; - val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) Ts; + val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) fpTs'; val ctr_Tsss = map (map (map dest_dtyp o snd) o #3 o snd) descr; val kkssss = map (map (map (fn Old_Datatype_Aux.DtRec kk => [kk] | _ => []) o snd) o #3 o snd) descr; @@ -146,34 +283,47 @@ val callssss = map2 (map2 (map2 (fn ctr_T => map (apply_comps (num_binder_types ctr_T))))) ctr_Tsss kkssss; - val b_names = Name.variant_list [] (map base_name_of_typ Ts); - val compat_b_names = map (prefix compatN) b_names; + val b_names = Name.variant_list [] (map base_name_of_typ fpTs'); + val compat_b_names = map (prefix compat_N) b_names; val compat_bs = map Binding.name compat_b_names; val ((fp_sugars, (lfp_sugar_thms, _)), lthy') = if nn > nn_fp then - mutualize_fp_sugars Least_FP cliques compat_bs Ts callers callssss fp_sugars0 lthy + mutualize_fp_sugars Least_FP cliques compat_bs fpTs' callers callssss fp_sugars0 lthy else ((fp_sugars0, (NONE, NONE)), lthy); - val recs = map (fst o dest_Const o #co_rec) fp_sugars; - val rec_thms = maps #co_rec_thms fp_sugars; - val {common_co_inducts = [induct], ...} :: _ = fp_sugars; val inducts = map (the_single o #co_inducts) fp_sugars; + val recs = map #co_rec fp_sugars; + val rec_thmss = map #co_rec_thms fp_sugars; + + fun is_nested_rec_type (Type (@{type_name fun}, [_, T])) = member (op =) fpTs' (body_type T) + | is_nested_rec_type _ = false; + + val ((induct', inducts', recs', rec'_thmss), lthy'') = + if nesting_pref = Unfold_Nesting andalso + exists (exists (exists is_nested_rec_type)) ctr_Tsss then + define_fun_rec_derive_thms induct inducts recs rec_thmss fpTs' lthy' + else + ((induct, inducts, recs, rec_thmss), lthy'); + + val rec'_names = map (fst o dest_Const) recs'; + val rec'_thms = flat rec'_thmss; + fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects, distincts, case_thms, case_cong, case_cong_weak, split, split_asm, ...}, ...} : fp_sugar) = (T_name0, - {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct, - inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs, - rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms, + {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct', + inducts = inducts', exhaust = exhaust, nchotomy = nchotomy, rec_names = rec'_names, + rec_rewrites = rec'_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms, case_cong = case_cong, case_cong_weak = case_cong_weak, split = split, split_asm = split_asm}); val infos = map_index mk_info (take nn_fp fp_sugars); in - (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') + (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy'') end; fun infos_of_new_datatype_mutual_cluster lthy fpT_name = @@ -298,7 +448,7 @@ NONE => [] | SOME ((induct_thms, induct_thm, induct_attrs), (rec_thmss, _)) => let - val common_name = compatN ^ mk_common_name b_names; + val common_name = compat_N ^ mk_common_name b_names; val common_notes = (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else []) diff -r a456b2c03491 -r c1f3fa32d322 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Sep 08 14:03:01 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Sep 08 14:03:01 2014 +0200 @@ -194,7 +194,7 @@ fun mk_spec ctr_offset ({T, fp_res_index, ctr_sugar = {ctrs, ...}, recx, rec_thms, ...} : basic_lfp_sugar) = - {recx = mk_co_rec thy Least_FP (substAT T) perm_Cs' recx, + {recx = mk_co_rec thy Least_FP perm_Cs' (substAT T) recx, fp_nesting_map_ident0s = fp_nesting_map_ident0s, fp_nesting_map_comps = fp_nesting_map_comps, ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms}; in diff -r a456b2c03491 -r c1f3fa32d322 src/HOL/Tools/Old_Datatype/old_datatype_aux.ML --- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Mon Sep 08 14:03:01 2014 +0200 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Mon Sep 08 14:03:01 2014 +0200 @@ -331,7 +331,8 @@ fun get_dt_descr T i tname dts = (case Symtab.lookup dt_info tname of NONE => - typ_error T (quote tname ^ " is not a datatype - can't use it in nested recursion") + typ_error T (quote tname ^ " is not registered as an old-style datatype and hence cannot \ + \be used in nested recursion") | SOME {index, descr, ...} => let val (_, vars, _) = the (AList.lookup (op =) descr index);