# HG changeset patch
# User blanchet
# Date 1347424056 -7200
# Node ID 56fcd826f90ce55658dc511b501f7b1b0e317f13
# Parent  6e30078de4f01d4c847077d1577469ca07f8fa2c
tuning

diff -r 6e30078de4f0 -r 56fcd826f90c src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- 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;
diff -r 6e30078de4f0 -r 56fcd826f90c src/HOL/Codatatype/Tools/bnf_gfp.ML
--- 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;
diff -r 6e30078de4f0 -r 56fcd826f90c src/HOL/Codatatype/Tools/bnf_lfp.ML
--- 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;
diff -r 6e30078de4f0 -r 56fcd826f90c src/HOL/Codatatype/Tools/bnf_wrap.ML
--- 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;