--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 05:29:21 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 06:27:36 2012 +0200
@@ -369,7 +369,6 @@
(case_binder :: ctr_binders) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss)
||> `Local_Theory.restore;
- (*transforms defined frees into consts (and more)*)
val phi = Proof_Context.export_morphism lthy lthy';
val ctr_defs = map (Morphism.thm phi) raw_ctr_defs;
@@ -446,7 +445,6 @@
#>> apsnd snd) binders specs
||> `Local_Theory.restore;
- (*transforms defined frees into consts (and more)*)
val phi = Proof_Context.export_morphism lthy lthy';
val [iter_def, rec_def] = map (Morphism.thm phi) defs;
@@ -490,7 +488,6 @@
#>> apsnd snd) binders specs
||> `Local_Theory.restore;
- (*transforms defined frees into consts (and more)*)
val phi = Proof_Context.export_morphism lthy lthy';
val [coiter_def, corec_def] = map (Morphism.thm phi) defs;
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Wed Sep 12 05:29:21 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Wed Sep 12 06:27:36 2012 +0200
@@ -312,11 +312,10 @@
end;
val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) =
- lthy
- |> Specification.definition (SOME (coalg_bind, NONE, NoSyn), (coalg_def_bind, coalg_spec))
- ||> `Local_Theory.restore;
-
- (*transforms defined frees into consts*)
+ lthy
+ |> Specification.definition (SOME (coalg_bind, NONE, NoSyn), (coalg_def_bind, coalg_spec))
+ ||> `Local_Theory.restore;
+
val phi = Proof_Context.export_morphism lthy_old lthy;
val coalg = fst (Term.dest_Const (Morphism.term phi coalg_free));
val coalg_def = Morphism.thm phi coalg_def_free;
@@ -396,11 +395,10 @@
end;
val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
- lthy
- |> Specification.definition (SOME (mor_bind, NONE, NoSyn), (mor_def_bind, mor_spec))
- ||> `Local_Theory.restore;
-
- (*transforms defined frees into consts*)
+ lthy
+ |> Specification.definition (SOME (mor_bind, NONE, NoSyn), (mor_def_bind, mor_spec))
+ ||> `Local_Theory.restore;
+
val phi = Proof_Context.export_morphism lthy_old lthy;
val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
val mor_def = Morphism.thm phi mor_def_free;
@@ -551,7 +549,6 @@
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val hset_rec_defs = map (Morphism.thm phi) hset_rec_def_frees;
@@ -601,7 +598,6 @@
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val hset_defss = map (map (Morphism.thm phi)) hset_def_frees;
@@ -820,11 +816,10 @@
end;
val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) =
- lthy
- |> Specification.definition (SOME (bis_bind, NONE, NoSyn), (bis_def_bind, bis_spec))
- ||> `Local_Theory.restore;
-
- (*transforms defined frees into consts*)
+ lthy
+ |> Specification.definition (SOME (bis_bind, NONE, NoSyn), (bis_def_bind, bis_spec))
+ ||> `Local_Theory.restore;
+
val phi = Proof_Context.export_morphism lthy_old lthy;
val bis = fst (Term.dest_Const (Morphism.term phi bis_free));
val bis_def = Morphism.thm phi bis_def_free;
@@ -961,7 +956,6 @@
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val lsbis_defs = map (Morphism.thm phi) lsbis_def_frees;
@@ -1045,7 +1039,6 @@
|> Specification.definition (SOME (sbd_bind, NONE, NoSyn), (sbd_def_bind, sbd_spec))
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val sbd_def = Morphism.thm phi sbd_def_free;
@@ -1177,7 +1170,6 @@
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val isNode_defs = map (Morphism.thm phi) isNode_def_frees;
@@ -1231,7 +1223,6 @@
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val carT_defs = map (Morphism.thm phi) carT_def_frees;
@@ -1272,7 +1263,6 @@
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val strT_defs = map ((fn def => trans OF [def RS fun_cong, @{thm prod.cases}]) o
@@ -1460,7 +1450,6 @@
|> Specification.definition (SOME (Lev_bind, NONE, NoSyn), (Lev_def_bind, Lev_spec))
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val Lev_def = Morphism.thm phi Lev_def_free;
@@ -1506,7 +1495,6 @@
|> Specification.definition (SOME (rv_bind, NONE, NoSyn), (rv_def_bind, rv_spec))
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val rv_def = Morphism.thm phi rv_def_free;
@@ -1557,7 +1545,6 @@
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val beh_defs = map (Morphism.thm phi) beh_def_frees;
@@ -1911,7 +1898,6 @@
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
fun mk_unfs passive =
map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o
@@ -1965,7 +1951,6 @@
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val coiters = map (Morphism.term phi) coiter_frees;
val coiter_names = map (fst o dest_Const) coiters;
@@ -2071,14 +2056,13 @@
end;
val ((fld_frees, (_, fld_def_frees)), (lthy, lthy_old)) =
- lthy
- |> fold_map2 (fn i => fn fldT =>
- Specification.definition
- (SOME (fld_bind i, NONE, NoSyn), (fld_def_bind i, fld_spec i fldT))) ks fldTs
- |>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
-
- (*transforms defined frees into consts*)
+ lthy
+ |> fold_map2 (fn i => fn fldT =>
+ Specification.definition
+ (SOME (fld_bind i, NONE, NoSyn), (fld_def_bind i, fld_spec i fldT))) ks fldTs
+ |>> apsnd split_list o split_list
+ ||> `Local_Theory.restore;
+
val phi = Proof_Context.export_morphism lthy_old lthy;
fun mk_flds params =
map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi)
@@ -2152,15 +2136,14 @@
end;
val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) =
- lthy
- |> fold_map3 (fn i => fn T => fn AT =>
- Specification.definition
- (SOME (corec_bind i, NONE, NoSyn), (corec_def_bind i, corec_spec i T AT)))
- ks Ts activeAs
- |>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
-
- (*transforms defined frees into consts*)
+ lthy
+ |> fold_map3 (fn i => fn T => fn AT =>
+ Specification.definition
+ (SOME (corec_bind i, NONE, NoSyn), (corec_def_bind i, corec_spec i T AT)))
+ ks Ts activeAs
+ |>> apsnd split_list o split_list
+ ||> `Local_Theory.restore;
+
val phi = Proof_Context.export_morphism lthy_old lthy;
val corecs = map (Morphism.term phi) corec_frees;
val corec_names = map (fst o dest_Const) corecs;
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Wed Sep 12 05:29:21 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Wed Sep 12 06:27:36 2012 +0200
@@ -234,7 +234,6 @@
|> Specification.definition (SOME (alg_bind, NONE, NoSyn), (alg_def_bind, alg_spec))
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val alg = fst (Term.dest_Const (Morphism.term phi alg_free));
val alg_def = Morphism.thm phi alg_def_free;
@@ -329,7 +328,6 @@
|> Specification.definition (SOME (mor_bind, NONE, NoSyn), (mor_def_bind, mor_spec))
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
val mor_def = Morphism.thm phi mor_def_free;
@@ -715,7 +713,6 @@
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees;
val min_alg_defs = map (Morphism.thm phi) min_alg_def_frees;
@@ -834,7 +831,6 @@
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val str_inits =
map (Term.subst_atomic_types (map (`(Morphism.typ phi)) params') o Morphism.term phi)
@@ -1011,15 +1007,14 @@
end;
val ((fld_frees, (_, fld_def_frees)), (lthy, lthy_old)) =
- lthy
- |> fold_map6 (fn i => fn abs => fn str => fn map => fn x => fn x' =>
- Specification.definition
- (SOME (fld_bind i, NONE, NoSyn), (fld_def_bind i, fld_spec i abs str map x x')))
- ks Abs_Ts str_inits map_FT_inits xFs xFs'
- |>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ lthy
+ |> fold_map6 (fn i => fn abs => fn str => fn map => fn x => fn x' =>
+ Specification.definition
+ (SOME (fld_bind i, NONE, NoSyn), (fld_def_bind i, fld_spec i abs str map x x')))
+ ks Abs_Ts str_inits map_FT_inits xFs xFs'
+ |>> apsnd split_list o split_list
+ ||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
fun mk_flds passive =
map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o
@@ -1070,15 +1065,14 @@
end;
val ((iter_frees, (_, iter_def_frees)), (lthy, lthy_old)) =
- lthy
- |> fold_map3 (fn i => fn T => fn AT =>
- Specification.definition
- (SOME (iter_bind i, NONE, NoSyn), (iter_def_bind i, iter_spec i T AT)))
- ks Ts activeAs
- |>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ lthy
+ |> fold_map3 (fn i => fn T => fn AT =>
+ Specification.definition
+ (SOME (iter_bind i, NONE, NoSyn), (iter_def_bind i, iter_spec i T AT)))
+ ks Ts activeAs
+ |>> apsnd split_list o split_list
+ ||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val iters = map (Morphism.term phi) iter_frees;
val iter_names = map (fst o dest_Const) iters;
@@ -1156,14 +1150,13 @@
end;
val ((unf_frees, (_, unf_def_frees)), (lthy, lthy_old)) =
- lthy
- |> fold_map3 (fn i => fn FT => fn T =>
- Specification.definition
- (SOME (unf_bind i, NONE, NoSyn), (unf_def_bind i, unf_spec i FT T))) ks FTs Ts
- |>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ lthy
+ |> fold_map3 (fn i => fn FT => fn T =>
+ Specification.definition
+ (SOME (unf_bind i, NONE, NoSyn), (unf_def_bind i, unf_spec i FT T))) ks FTs Ts
+ |>> apsnd split_list o split_list
+ ||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
fun mk_unfs params =
map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi)
@@ -1232,15 +1225,14 @@
end;
val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) =
- lthy
- |> fold_map3 (fn i => fn T => fn AT =>
- Specification.definition
- (SOME (rec_bind i, NONE, NoSyn), (rec_def_bind i, rec_spec i T AT)))
- ks Ts activeAs
- |>> apsnd split_list o split_list
- ||> `Local_Theory.restore;
+ lthy
+ |> fold_map3 (fn i => fn T => fn AT =>
+ Specification.definition
+ (SOME (rec_bind i, NONE, NoSyn), (rec_def_bind i, rec_spec i T AT)))
+ ks Ts activeAs
+ |>> apsnd split_list o split_list
+ ||> `Local_Theory.restore;
- (*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
val recs = map (Morphism.term phi) rec_frees;
val rec_names = map (fst o dest_Const) recs;
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 12 05:29:21 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 12 06:27:36 2012 +0200
@@ -269,7 +269,6 @@
((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
||> `Local_Theory.restore;
- (*transforms defined frees into consts (and more)*)
val phi = Proof_Context.export_morphism lthy lthy';
val disc_defs = map (Morphism.thm phi) raw_disc_defs;