# HG changeset patch
# User blanchet
# Date 1437060998 -7200
# Node ID a2a3766890821ac49d9f40cd5fe356c3dc5c991d
# Parent  685b169d06112100e97cb0c2fe79283f5c5acb1f# Parent  6aaa9b95cf4763d63668f91d4575fe904e01da66
merge

diff -r 6aaa9b95cf47 -r a2a376689082 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Jul 16 17:02:07 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Jul 16 17:36:38 2015 +0200
@@ -3186,8 +3186,8 @@
 processed more efficiently.
 
 \item
-\emph{Locally fixed types cannot be used in (co)datatype specifications.}
-This limitation can be circumvented by adding type arguments to the local
+\emph{Locally fixed types and terms cannot be used in type specifications.}
+The limitation on types can be circumvented by adding type arguments to the local
 (co)datatypes to abstract over the locally fixed types.
 
 \item
diff -r 6aaa9b95cf47 -r a2a376689082 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 16 17:02:07 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 16 17:36:38 2015 +0200
@@ -1663,6 +1663,25 @@
       (transpose setss)
   end;
 
+fun mk_coinduct_strong_thm coind rel_eqs rel_monos mk_vimage2p ctxt =
+  let
+    val n = Thm.nprems_of coind;
+    val m = Thm.nprems_of (hd rel_monos) - n;
+    fun mk_inst phi =
+      (phi, Thm.cterm_of ctxt (mk_union (Var phi, HOLogic.eq_const (fst (dest_pred2T (#2 phi))))));
+    val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map mk_inst;
+    fun mk_unfold rel_eq rel_mono =
+      let
+        val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl];
+        val mono = rel_mono OF (replicate m @{thm order_refl} @ replicate n @{thm eq_subset});
+      in mk_vimage2p (eq RS (mono RS @{thm predicate2D})) RS eqTrueI end;
+    val unfolds = map2 mk_unfold rel_eqs rel_monos @ @{thms sup_fun_def sup_bool_def
+      imp_disjL all_conj_distrib subst_eq_imp simp_thms(18,21,35)};
+  in
+    Thm.instantiate ([], insts) coind
+    |> unfold_thms ctxt unfolds
+  end;
+
 fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, (((pgss, _, _, _), cqgsss), _))
     dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
     kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
diff -r 6aaa9b95cf47 -r a2a376689082 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Jul 16 17:02:07 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Jul 16 17:36:38 2015 +0200
@@ -194,8 +194,6 @@
   val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
     thm list -> thm list -> thm list
 
-  val mk_coinduct_strong_thm: thm -> thm list -> thm list -> (thm -> thm) -> Proof.context -> thm
-
   val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 'a) ->
     binding list -> (string * sort) list -> (string * sort) list -> ((string * sort) * typ) list ->
@@ -603,25 +601,6 @@
     split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems)
   end;
 
-fun mk_coinduct_strong_thm coind rel_eqs rel_monos mk_vimage2p ctxt =
-  let
-    val n = Thm.nprems_of coind;
-    val m = Thm.nprems_of (hd rel_monos) - n;
-    fun mk_inst phi =
-      (phi, Thm.cterm_of ctxt (mk_union (Var phi, HOLogic.eq_const (fst (dest_pred2T (#2 phi))))))
-    val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map mk_inst;
-    fun mk_unfold rel_eq rel_mono =
-      let
-        val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl];
-        val mono = rel_mono OF (replicate m @{thm order_refl} @ replicate n @{thm eq_subset});
-      in mk_vimage2p (eq RS (mono RS @{thm predicate2D})) RS eqTrueI end;
-    val unfolds = map2 mk_unfold rel_eqs rel_monos @ @{thms sup_fun_def sup_bool_def
-      imp_disjL all_conj_distrib subst_eq_imp simp_thms(18,21,35)};
-  in
-    Thm.instantiate ([], insts) coind
-    |> unfold_thms ctxt unfolds
-  end;
-
 fun fp_bnf construct_fp bs resBs Ds0 fp_eqs lthy =
   let
     val time = time lthy;
diff -r 6aaa9b95cf47 -r a2a376689082 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Jul 16 17:02:07 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Jul 16 17:36:38 2015 +0200
@@ -82,9 +82,11 @@
     etac ctxt notE THEN' atac ORELSE'
     etac ctxt disjE))));
 
-fun ss_fst_snd_conv ctxt = simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
+fun ss_fst_snd_conv ctxt =
+  Raw_Simplifier.simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
 
-fun case_atac ctxt = simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt);
+fun case_atac ctxt =
+  Simplifier.full_simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt);
 
 fun same_case_tac ctxt m =
   HEADGOAL (if m = 0 then rtac ctxt TrueI