1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Fri Aug 30 15:05:04 2013 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Fri Aug 30 15:36:00 2013 +0200
     1.3 @@ -739,7 +739,7 @@
     1.4    * e.g.
     1.5  *}
     1.6  
     1.7 -    primrec_new_notyet
     1.8 +    primrec_new
     1.9        at_tree\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" and
    1.10        at_trees\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f list \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> 'a"
    1.11      where
    1.12 @@ -752,7 +752,7 @@
    1.13              Zero \<Rightarrow> at_tree\<^sub>f\<^sub>f t
    1.14            | Suc j' \<Rightarrow> at_trees\<^sub>f\<^sub>f ts j')"
    1.15  
    1.16 -    primrec_new_notyet
    1.17 +    primrec_new
    1.18        sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" and
    1.19        sum_btree_option :: "'a btree option \<Rightarrow> 'a"
    1.20      where

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Fri Aug 30 15:05:04 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Fri Aug 30 15:36:00 2013 +0200
     2.3 @@ -276,13 +276,13 @@
     2.4        |>> apfst rev o apsnd rev;
     2.5      val foldN = fp_case fp ctor_foldN dtor_unfoldN;
     2.6      val recN = fp_case fp ctor_recN dtor_corecN;
     2.7 -    val (((raw_un_folds, raw_un_fold_defs), (raw_co_recs, raw_co_rec_defs)), (lthy, lthy_old)) =
     2.8 +    val (((raw_un_folds, raw_un_fold_defs), (raw_co_recs, raw_co_rec_defs)), (lthy, raw_lthy)) =
     2.9        lthy
    2.10        |> mk_iters false foldN
    2.11        ||>> mk_iters true recN
    2.12 -      ||> `(Local_Theory.restore);
    2.13 +      ||> `Local_Theory.restore;
    2.14  
    2.15 -    val phi = Proof_Context.export_morphism lthy_old lthy;
    2.16 +    val phi = Proof_Context.export_morphism raw_lthy lthy;
    2.17  
    2.18      val un_folds = map (Morphism.term phi) raw_un_folds;
    2.19      val co_recs = map (Morphism.term phi) raw_co_recs;
    2.20 @@ -316,7 +316,7 @@
    2.21            Library.foldr1 HOLogic.mk_conj goals
    2.22            |> HOLogic.mk_Trueprop
    2.23            |> fold_rev Logic.all ss
    2.24 -          |> (fn goal => Goal.prove_sorry lthy [] [] goal tac)
    2.25 +          |> (fn goal => Goal.prove_sorry raw_lthy [] [] goal tac)
    2.26            |> Thm.close_derivation
    2.27            |> Morphism.thm phi
    2.28            |> split_conj_thm