# HG changeset patch
# User traytel
# Date 1377869760 -7200
# Node ID 20440c789759482dfe4765858ece2e5c0f935288
# Parent  77da8d3c46e08a5559fb6ba43391967dc1aa5d6a
prove theorem in the right context (that knows about local variables)

diff -r 77da8d3c46e0 -r 20440c789759 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Aug 30 15:05:04 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Aug 30 15:36:00 2013 +0200
@@ -739,7 +739,7 @@
   * e.g.
 *}
 
-    primrec_new_notyet
+    primrec_new
       at_tree\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" and
       at_trees\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f list \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> 'a"
     where
@@ -752,7 +752,7 @@
             Zero \<Rightarrow> at_tree\<^sub>f\<^sub>f t
           | Suc j' \<Rightarrow> at_trees\<^sub>f\<^sub>f ts j')"
 
-    primrec_new_notyet
+    primrec_new
       sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" and
       sum_btree_option :: "'a btree option \<Rightarrow> 'a"
     where
diff -r 77da8d3c46e0 -r 20440c789759 src/HOL/BNF/Tools/bnf_fp_n2m.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Fri Aug 30 15:05:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Fri Aug 30 15:36:00 2013 +0200
@@ -276,13 +276,13 @@
       |>> apfst rev o apsnd rev;
     val foldN = fp_case fp ctor_foldN dtor_unfoldN;
     val recN = fp_case fp ctor_recN dtor_corecN;
-    val (((raw_un_folds, raw_un_fold_defs), (raw_co_recs, raw_co_rec_defs)), (lthy, lthy_old)) =
+    val (((raw_un_folds, raw_un_fold_defs), (raw_co_recs, raw_co_rec_defs)), (lthy, raw_lthy)) =
       lthy
       |> mk_iters false foldN
       ||>> mk_iters true recN
-      ||> `(Local_Theory.restore);
+      ||> `Local_Theory.restore;
 
-    val phi = Proof_Context.export_morphism lthy_old lthy;
+    val phi = Proof_Context.export_morphism raw_lthy lthy;
 
     val un_folds = map (Morphism.term phi) raw_un_folds;
     val co_recs = map (Morphism.term phi) raw_co_recs;
@@ -316,7 +316,7 @@
           Library.foldr1 HOLogic.mk_conj goals
           |> HOLogic.mk_Trueprop
           |> fold_rev Logic.all ss
-          |> (fn goal => Goal.prove_sorry lthy [] [] goal tac)
+          |> (fn goal => Goal.prove_sorry raw_lthy [] [] goal tac)
           |> Thm.close_derivation
           |> Morphism.thm phi
           |> split_conj_thm