author traytel Fri, 30 Aug 2013 15:36:00 +0200 changeset 53331 20440c789759 parent 53330 77da8d3c46e0 child 53332 c97a05a26dd6
prove theorem in the right context (that knows about local variables)
 src/Doc/Datatypes/Datatypes.thy file | annotate | diff | comparison | revisions src/HOL/BNF/Tools/bnf_fp_n2m.ML file | annotate | diff | comparison | revisions
```--- 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```
```--- 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```