src/HOL/Codatatype/Tools/bnf_lfp.ML
changeset 49337 538687a77075
parent 49331 f4169aa67513
child 49341 d406979024d1
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 17:26:05 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 17:26:05 2012 +0200
     1.3 @@ -10,8 +10,8 @@
     1.4  sig
     1.5    val bnf_lfp: mixfix list -> (string * sort) list option -> binding list ->
     1.6      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     1.7 -    (term list * term list * term list * term list * thm list * thm list * thm list * thm list *
     1.8 -      thm list) * local_theory
     1.9 +    (term list * term list * term list * term list * thm * thm list * thm list * thm list *
    1.10 +      thm list * thm list) * local_theory
    1.11  end;
    1.12  
    1.13  structure BNF_LFP : BNF_LFP =
    1.14 @@ -33,7 +33,7 @@
    1.15      val n = length bnfs; (*active*)
    1.16      val ks = 1 upto n;
    1.17      val m = live - n; (*passive, if 0 don't generate a new bnf*)
    1.18 -    val b = Binding.name (mk_bundle_name bs);
    1.19 +    val b = Binding.name (mk_common_name bs);
    1.20  
    1.21      (* TODO: check if m, n etc are sane *)
    1.22  
    1.23 @@ -1810,7 +1810,8 @@
    1.24              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    1.25            bs thmss)
    1.26    in
    1.27 -    ((unfs, flds, iters, recs, unf_fld_thms, fld_unf_thms, fld_inject_thms, iter_thms, rec_thms),
    1.28 +    ((unfs, flds, iters, recs, fld_induct_thm, unf_fld_thms, fld_unf_thms, fld_inject_thms,
    1.29 +      iter_thms, rec_thms),
    1.30       lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    1.31    end;
    1.32