merge
authorblanchet
Fri Jan 31 13:45:39 2014 +0100 (2014-01-31)
changeset 55209bfafffd5421d
parent 55208 11dd3d1da83b
parent 55204 345ee77213b5
child 55210 d1e3b708d74b
merge
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Jan 31 13:42:47 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Jan 31 13:45:39 2014 +0100
     1.3 @@ -163,7 +163,6 @@
     1.4      val Zeros = map (fn empty =>
     1.5       HOLogic.mk_tuple (map (fn U => absdummy U empty) activeAs)) emptys;
     1.6      val hrecTs = map fastype_of Zeros;
     1.7 -    val hsetTs = map (fn hrecT => Library.foldr (op -->) (sTs, HOLogic.natT --> hrecT)) hrecTs;
     1.8  
     1.9      val (((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')),
    1.10        As), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy),
    1.11 @@ -297,32 +296,28 @@
    1.12      (* coalgebra *)
    1.13  
    1.14      val coalg_bind = mk_internal_b (coN ^ algN) ;
    1.15 -    val coalg_name = Binding.name_of coalg_bind;
    1.16      val coalg_def_bind = (Thm.def_binding coalg_bind, []);
    1.17  
    1.18      (*forall i = 1 ... n: (\<forall>x \<in> Bi. si \<in> Fi_in A1 .. Am B1 ... Bn)*)
    1.19      val coalg_spec =
    1.20        let
    1.21 -        val coalgT = Library.foldr (op -->) (ATs @ BTs @ sTs, HOLogic.boolT);
    1.22 -
    1.23          val ins = map3 mk_in (replicate n (As @ Bs)) setssAs FTsAs;
    1.24          fun mk_coalg_conjunct B s X z z' =
    1.25            mk_Ball B (Term.absfree z' (HOLogic.mk_mem (s $ z, X)));
    1.26  
    1.27 -        val lhs = Term.list_comb (Free (coalg_name, coalgT), As @ Bs @ ss);
    1.28          val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_coalg_conjunct Bs ss ins zs zs')
    1.29        in
    1.30 -        mk_Trueprop_eq (lhs, rhs)
    1.31 +        fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss) rhs
    1.32        end;
    1.33  
    1.34      val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) =
    1.35        lthy
    1.36 -      |> Specification.definition (SOME (coalg_bind, NONE, NoSyn), (coalg_def_bind, coalg_spec))
    1.37 +      |> Local_Theory.define ((coalg_bind, NoSyn), (coalg_def_bind, coalg_spec))
    1.38        ||> `Local_Theory.restore;
    1.39  
    1.40      val phi = Proof_Context.export_morphism lthy_old lthy;
    1.41      val coalg = fst (Term.dest_Const (Morphism.term phi coalg_free));
    1.42 -    val coalg_def = Morphism.thm phi coalg_def_free;
    1.43 +    val coalg_def = mk_unabs_def (live + n) (Morphism.thm phi coalg_def_free RS meta_eq_to_obj_eq);
    1.44  
    1.45      fun mk_coalg As Bs ss =
    1.46        let
    1.47 @@ -373,7 +368,6 @@
    1.48      (* morphism *)
    1.49  
    1.50      val mor_bind = mk_internal_b morN;
    1.51 -    val mor_name = Binding.name_of mor_bind;
    1.52      val mor_def_bind = (Thm.def_binding mor_bind, []);
    1.53  
    1.54      (*fbetw) forall i = 1 ... n: (\<forall>x \<in> Bi. fi x \<in> B'i)*)
    1.55 @@ -381,29 +375,26 @@
    1.56         Fi_map id ... id f1 ... fn (si x) = si' (fi x)*)
    1.57      val mor_spec =
    1.58        let
    1.59 -        val morT = Library.foldr (op -->) (BTs @ sTs @ B'Ts @ s'Ts @ fTs, HOLogic.boolT);
    1.60 -
    1.61          fun mk_fbetw f B1 B2 z z' =
    1.62            mk_Ball B1 (Term.absfree z' (HOLogic.mk_mem (f $ z, B2)));
    1.63          fun mk_mor B mapAsBs f s s' z z' =
    1.64            mk_Ball B (Term.absfree z' (HOLogic.mk_eq
    1.65              (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ z]), s' $ (f $ z))));
    1.66 -        val lhs = Term.list_comb (Free (mor_name, morT), Bs @ ss @ B's @ s's @ fs);
    1.67          val rhs = HOLogic.mk_conj
    1.68            (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'),
    1.69             Library.foldr1 HOLogic.mk_conj (map7 mk_mor Bs mapsAsBs fs ss s's zs zs'))
    1.70        in
    1.71 -        mk_Trueprop_eq (lhs, rhs)
    1.72 +        fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs
    1.73        end;
    1.74  
    1.75      val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
    1.76        lthy
    1.77 -      |> Specification.definition (SOME (mor_bind, NONE, NoSyn), (mor_def_bind, mor_spec))
    1.78 +      |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
    1.79        ||> `Local_Theory.restore;
    1.80  
    1.81      val phi = Proof_Context.export_morphism lthy_old lthy;
    1.82      val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
    1.83 -    val mor_def = Morphism.thm phi mor_def_free;
    1.84 +    val mor_def = mk_unabs_def (5 * n) (Morphism.thm phi mor_def_free RS meta_eq_to_obj_eq);
    1.85  
    1.86      fun mk_mor Bs1 ss1 Bs2 ss2 fs =
    1.87        let
    1.88 @@ -518,10 +509,9 @@
    1.89      val timer = time (timer "Morphism definition & thms");
    1.90  
    1.91      fun hset_rec_bind j = mk_internal_b (hset_recN ^ (if m = 1 then "" else string_of_int j));
    1.92 -    val hset_rec_name = Binding.name_of o hset_rec_bind;
    1.93      val hset_rec_def_bind = rpair [] o Thm.def_binding o hset_rec_bind;
    1.94  
    1.95 -    fun hset_rec_spec j Zero hsetT hrec hrec' =
    1.96 +    fun hset_rec_spec j Zero hrec hrec' =
    1.97        let
    1.98          fun mk_Suc s setsAs z z' =
    1.99            let
   1.100 @@ -535,24 +525,23 @@
   1.101          val Suc = Term.absdummy HOLogic.natT (Term.absfree hrec'
   1.102            (HOLogic.mk_tuple (map4 mk_Suc ss setssAs zs zs')));
   1.103  
   1.104 -        val lhs = Term.list_comb (Free (hset_rec_name j, hsetT), ss);
   1.105          val rhs = mk_nat_rec Zero Suc;
   1.106        in
   1.107 -        mk_Trueprop_eq (lhs, rhs)
   1.108 +        fold_rev (Term.absfree o Term.dest_Free) ss rhs
   1.109        end;
   1.110  
   1.111      val ((hset_rec_frees, (_, hset_rec_def_frees)), (lthy, lthy_old)) =
   1.112        lthy
   1.113 -      |> fold_map5 (fn j => fn Zero => fn hsetT => fn hrec => fn hrec' => Specification.definition
   1.114 -        (SOME (hset_rec_bind j, NONE, NoSyn),
   1.115 -          (hset_rec_def_bind j, hset_rec_spec j Zero hsetT hrec hrec')))
   1.116 -        ls Zeros hsetTs hrecs hrecs'
   1.117 +      |> fold_map4 (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define
   1.118 +        ((hset_rec_bind j, NoSyn), (hset_rec_def_bind j, hset_rec_spec j Zero hrec hrec')))
   1.119 +        ls Zeros hrecs hrecs'
   1.120        |>> apsnd split_list o split_list
   1.121        ||> `Local_Theory.restore;
   1.122  
   1.123      val phi = Proof_Context.export_morphism lthy_old lthy;
   1.124  
   1.125 -    val hset_rec_defs = map (Morphism.thm phi) hset_rec_def_frees;
   1.126 +    val hset_rec_defs = map (fn def =>
   1.127 +      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) hset_rec_def_frees;
   1.128      val hset_recs = map (fst o Term.dest_Const o Morphism.term phi) hset_rec_frees;
   1.129  
   1.130      fun mk_hset_rec ss nat i j T =
   1.131 @@ -573,35 +562,31 @@
   1.132  
   1.133      fun hset_binds j = mk_internal_bs (hsetN ^ (if m = 1 then "" else string_of_int j))
   1.134      fun hset_bind i j = nth (hset_binds j) (i - 1);
   1.135 -    val hset_name = Binding.name_of oo hset_bind;
   1.136      val hset_def_bind = rpair [] o Thm.def_binding oo hset_bind;
   1.137  
   1.138      fun hset_spec i j =
   1.139        let
   1.140 -        val U = nth activeAs (i - 1);
   1.141          val z = nth zs (i - 1);
   1.142          val T = nth passiveAs (j - 1);
   1.143 -        val setT = HOLogic.mk_setT T;
   1.144 -        val hsetT = Library.foldr (op -->) (sTs, U --> setT);
   1.145 -
   1.146 -        val lhs = Term.list_comb (Free (hset_name i j, hsetT), ss @ [z]);
   1.147 +
   1.148          val rhs = mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
   1.149            (Term.absfree nat' (mk_hset_rec ss nat i j T $ z));
   1.150        in
   1.151 -        mk_Trueprop_eq (lhs, rhs)
   1.152 +        fold_rev (Term.absfree o Term.dest_Free) (ss @ [z]) rhs
   1.153        end;
   1.154  
   1.155      val ((hset_frees, (_, hset_def_frees)), (lthy, lthy_old)) =
   1.156        lthy
   1.157 -      |> fold_map (fn i => fold_map (fn j => Specification.definition
   1.158 -        (SOME (hset_bind i j, NONE, NoSyn), (hset_def_bind i j, hset_spec i j))) ls) ks
   1.159 +      |> fold_map (fn i => fold_map (fn j => Local_Theory.define
   1.160 +        ((hset_bind i j, NoSyn), (hset_def_bind i j, hset_spec i j))) ls) ks
   1.161        |>> map (apsnd split_list o split_list)
   1.162        |>> apsnd split_list o split_list
   1.163        ||> `Local_Theory.restore;
   1.164  
   1.165      val phi = Proof_Context.export_morphism lthy_old lthy;
   1.166  
   1.167 -    val hset_defss = map (map (Morphism.thm phi)) hset_def_frees;
   1.168 +    val hset_defss = map (map (fn def =>
   1.169 +      mk_unabs_def (n + 1) (Morphism.thm phi def RS meta_eq_to_obj_eq))) hset_def_frees;
   1.170      val hset_defss' = transpose hset_defss;
   1.171      val hset_namess = map (map (fst o Term.dest_Const o Morphism.term phi)) hset_frees;
   1.172  
   1.173 @@ -723,7 +708,6 @@
   1.174      (* bisimulation *)
   1.175  
   1.176      val bis_bind = mk_internal_b bisN;
   1.177 -    val bis_name = Binding.name_of bis_bind;
   1.178      val bis_def_bind = (Thm.def_binding bis_bind, []);
   1.179  
   1.180      fun mk_bis_le_conjunct R B1 B2 = mk_leq R (mk_Times (B1, B2));
   1.181 @@ -731,8 +715,6 @@
   1.182  
   1.183      val bis_spec =
   1.184        let
   1.185 -        val bisT = Library.foldr (op -->) (ATs @ BTs @ sTs @ B'Ts @ s'Ts @ setRTs, HOLogic.boolT);
   1.186 -
   1.187          val fst_args = passive_ids @ fsts;
   1.188          val snd_args = passive_ids @ snds;
   1.189          fun mk_bis R s s' b1 b2 RF map1 map2 sets =
   1.190 @@ -743,22 +725,21 @@
   1.191                  (HOLogic.mk_eq (Term.list_comb (map1, fst_args) $ RF, s $ b1),
   1.192                  HOLogic.mk_eq (Term.list_comb (map2, snd_args) $ RF, s' $ b2))))));
   1.193  
   1.194 -        val lhs = Term.list_comb (Free (bis_name, bisT), As @ Bs @ ss @ B's @ s's @ Rs);
   1.195          val rhs = HOLogic.mk_conj
   1.196            (bis_le, Library.foldr1 HOLogic.mk_conj
   1.197              (map9 mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss))
   1.198        in
   1.199 -        mk_Trueprop_eq (lhs, rhs)
   1.200 +        fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss @ B's @ s's @ Rs) rhs
   1.201        end;
   1.202  
   1.203      val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) =
   1.204        lthy
   1.205 -      |> Specification.definition (SOME (bis_bind, NONE, NoSyn), (bis_def_bind, bis_spec))
   1.206 +      |> Local_Theory.define ((bis_bind, NoSyn), (bis_def_bind, bis_spec))
   1.207        ||> `Local_Theory.restore;
   1.208  
   1.209      val phi = Proof_Context.export_morphism lthy_old lthy;
   1.210      val bis = fst (Term.dest_Const (Morphism.term phi bis_free));
   1.211 -    val bis_def = Morphism.thm phi bis_def_free;
   1.212 +    val bis_def = mk_unabs_def (m + 5 * n) (Morphism.thm phi bis_def_free RS meta_eq_to_obj_eq);
   1.213  
   1.214      fun mk_bis As Bs1 ss1 Bs2 ss2 Rs =
   1.215        let
   1.216 @@ -869,32 +850,26 @@
   1.217  
   1.218      val lsbis_binds = mk_internal_bs lsbisN;
   1.219      fun lsbis_bind i = nth lsbis_binds (i - 1);
   1.220 -    val lsbis_name = Binding.name_of o lsbis_bind;
   1.221      val lsbis_def_bind = rpair [] o Thm.def_binding o lsbis_bind;
   1.222  
   1.223      val all_sbis = HOLogic.mk_Collect (fst Rtuple', snd Rtuple', list_exists_free sRs
   1.224        (HOLogic.mk_conj (HOLogic.mk_eq (Rtuple, HOLogic.mk_tuple sRs), mk_sbis As Bs ss sRs)));
   1.225  
   1.226 -    fun lsbis_spec i RT =
   1.227 -      let
   1.228 -        fun mk_lsbisT RT =
   1.229 -          Library.foldr (op -->) (map fastype_of (As @ Bs @ ss), RT);
   1.230 -        val lhs = Term.list_comb (Free (lsbis_name i, mk_lsbisT RT), As @ Bs @ ss);
   1.231 -        val rhs = mk_UNION all_sbis (Term.absfree Rtuple' (mk_nthN n Rtuple i));
   1.232 -      in
   1.233 -        mk_Trueprop_eq (lhs, rhs)
   1.234 -      end;
   1.235 +    fun lsbis_spec i =
   1.236 +      fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss)
   1.237 +        (mk_UNION all_sbis (Term.absfree Rtuple' (mk_nthN n Rtuple i)));
   1.238  
   1.239      val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) =
   1.240        lthy
   1.241 -      |> fold_map2 (fn i => fn RT => Specification.definition
   1.242 -        (SOME (lsbis_bind i, NONE, NoSyn), (lsbis_def_bind i, lsbis_spec i RT))) ks setsRTs
   1.243 +      |> fold_map (fn i => Local_Theory.define
   1.244 +        ((lsbis_bind i, NoSyn), (lsbis_def_bind i, lsbis_spec i))) ks
   1.245        |>> apsnd split_list o split_list
   1.246        ||> `Local_Theory.restore;
   1.247  
   1.248      val phi = Proof_Context.export_morphism lthy_old lthy;
   1.249  
   1.250 -    val lsbis_defs = map (Morphism.thm phi) lsbis_def_frees;
   1.251 +    val lsbis_defs = map (fn def =>
   1.252 +      mk_unabs_def (live + n) (Morphism.thm phi def RS meta_eq_to_obj_eq)) lsbis_def_frees;
   1.253      val lsbiss = map (fst o Term.dest_Const o Morphism.term phi) lsbis_frees;
   1.254  
   1.255      fun mk_lsbis As Bs ss i =
   1.256 @@ -963,20 +938,18 @@
   1.257            val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
   1.258  
   1.259            val sbd_bind = mk_internal_b sum_bdN;
   1.260 -          val sbd_name = Binding.name_of sbd_bind;
   1.261            val sbd_def_bind = (Thm.def_binding sbd_bind, []);
   1.262  
   1.263 -          val sbd_spec = HOLogic.mk_Trueprop
   1.264 -            (HOLogic.mk_eq (Free (sbd_name, mk_relT (`I sbdT)), mk_dir_image sum_bd Abs_sbdT));
   1.265 +          val sbd_spec = mk_dir_image sum_bd Abs_sbdT;
   1.266  
   1.267            val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) =
   1.268              lthy
   1.269 -            |> Specification.definition (SOME (sbd_bind, NONE, NoSyn), (sbd_def_bind, sbd_spec))
   1.270 +            |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec))
   1.271              ||> `Local_Theory.restore;
   1.272  
   1.273            val phi = Proof_Context.export_morphism lthy_old lthy;
   1.274  
   1.275 -          val sbd_def = Morphism.thm phi sbd_def_free;
   1.276 +          val sbd_def = Morphism.thm phi sbd_def_free RS meta_eq_to_obj_eq;
   1.277            val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT));
   1.278  
   1.279            val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
   1.280 @@ -1031,12 +1004,10 @@
   1.281      val root = HOLogic.mk_set sum_sbd_listT [HOLogic.mk_list sum_sbdT []];
   1.282      val Zero = HOLogic.mk_tuple (map (fn U => absdummy U root) activeAs);
   1.283      val Lev_recT = fastype_of Zero;
   1.284 -    val LevT = Library.foldr (op -->) (sTs, HOLogic.natT --> Lev_recT);
   1.285  
   1.286      val Nil = HOLogic.mk_tuple (map3 (fn i => fn z => fn z'=>
   1.287        Term.absfree z' (mk_InN activeAs z i)) ks zs zs');
   1.288      val rv_recT = fastype_of Nil;
   1.289 -    val rvT = Library.foldr (op -->) (sTs, sum_sbd_listT --> rv_recT);
   1.290  
   1.291      val (((((((((((sumx, sumx'), (kks, kks')), (kl, kl')), (kl_copy, kl'_copy)), (Kl, Kl')),
   1.292        (lab, lab')), (Kl_lab, Kl_lab')), xs), (Lev_rec, Lev_rec')), (rv_rec, rv_rec')),
   1.293 @@ -1060,7 +1031,6 @@
   1.294  
   1.295      val isNode_binds = mk_internal_bs isNodeN;
   1.296      fun isNode_bind i = nth isNode_binds (i - 1);
   1.297 -    val isNode_name = Binding.name_of o isNode_bind;
   1.298      val isNode_def_bind = rpair [] o Thm.def_binding o isNode_bind;
   1.299  
   1.300      val isNodeT =
   1.301 @@ -1073,25 +1043,25 @@
   1.302      fun isNode_spec sets x i =
   1.303        let
   1.304          val (passive_sets, active_sets) = chop m (map (fn set => set $ x) sets);
   1.305 -        val lhs = Term.list_comb (Free (isNode_name i, isNodeT), As @ [Kl, lab, kl]);
   1.306          val rhs = list_exists_free [x]
   1.307            (Library.foldr1 HOLogic.mk_conj (HOLogic.mk_eq (lab $ kl, mk_InN bdFTs x i) ::
   1.308            map2 mk_leq passive_sets As @ map2 (curry HOLogic.mk_eq) active_sets Succs));
   1.309        in
   1.310 -        mk_Trueprop_eq (lhs, rhs)
   1.311 +        fold_rev (Term.absfree o Term.dest_Free) (As @ [Kl, lab, kl]) rhs
   1.312        end;
   1.313  
   1.314      val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
   1.315        lthy
   1.316 -      |> fold_map3 (fn i => fn x => fn sets => Specification.definition
   1.317 -        (SOME (isNode_bind i, NONE, NoSyn), (isNode_def_bind i, isNode_spec sets x i)))
   1.318 +      |> fold_map3 (fn i => fn x => fn sets => Local_Theory.define
   1.319 +        ((isNode_bind i, NoSyn), (isNode_def_bind i, isNode_spec sets x i)))
   1.320          ks xs isNode_setss
   1.321        |>> apsnd split_list o split_list
   1.322        ||> `Local_Theory.restore;
   1.323  
   1.324      val phi = Proof_Context.export_morphism lthy_old lthy;
   1.325  
   1.326 -    val isNode_defs = map (Morphism.thm phi) isNode_def_frees;
   1.327 +    val isNode_defs = map (fn def =>
   1.328 +      mk_unabs_def (m + 3) (Morphism.thm phi def RS meta_eq_to_obj_eq)) isNode_def_frees;
   1.329      val isNodes = map (fst o Term.dest_Const o Morphism.term phi) isNode_frees;
   1.330  
   1.331      fun mk_isNode As kl i =
   1.332 @@ -1120,31 +1090,28 @@
   1.333  
   1.334      val carT_binds = mk_internal_bs carTN;
   1.335      fun carT_bind i = nth carT_binds (i - 1);
   1.336 -    val carT_name = Binding.name_of o carT_bind;
   1.337      val carT_def_bind = rpair [] o Thm.def_binding o carT_bind;
   1.338  
   1.339      fun carT_spec i =
   1.340        let
   1.341 -        val carTT = Library.foldr (op -->) (ATs, HOLogic.mk_setT treeT);
   1.342 -
   1.343 -        val lhs = Term.list_comb (Free (carT_name i, carTT), As);
   1.344          val rhs = HOLogic.mk_Collect (fst Kl_lab', snd Kl_lab', list_exists_free [Kl, lab]
   1.345            (HOLogic.mk_conj (HOLogic.mk_eq (Kl_lab, HOLogic.mk_prod (Kl, lab)),
   1.346              HOLogic.mk_conj (isTree, mk_isNode As (HOLogic.mk_list sum_sbdT []) i))));
   1.347        in
   1.348 -        mk_Trueprop_eq (lhs, rhs)
   1.349 +        fold_rev (Term.absfree o Term.dest_Free) As rhs
   1.350        end;
   1.351  
   1.352      val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) =
   1.353        lthy
   1.354 -      |> fold_map (fn i => Specification.definition
   1.355 -        (SOME (carT_bind i, NONE, NoSyn), (carT_def_bind i, carT_spec i))) ks
   1.356 +      |> fold_map (fn i =>
   1.357 +        Local_Theory.define ((carT_bind i, NoSyn), (carT_def_bind i, carT_spec i))) ks
   1.358        |>> apsnd split_list o split_list
   1.359        ||> `Local_Theory.restore;
   1.360  
   1.361      val phi = Proof_Context.export_morphism lthy_old lthy;
   1.362  
   1.363 -    val carT_defs = map (Morphism.thm phi) carT_def_frees;
   1.364 +    val carT_defs = map (fn def =>
   1.365 +      mk_unabs_def m (Morphism.thm phi def RS meta_eq_to_obj_eq)) carT_def_frees;
   1.366      val carTs = map (fst o Term.dest_Const o Morphism.term phi) carT_frees;
   1.367  
   1.368      fun mk_carT As i = Term.list_comb
   1.369 @@ -1153,13 +1120,10 @@
   1.370  
   1.371      val strT_binds = mk_internal_bs strTN;
   1.372      fun strT_bind i = nth strT_binds (i - 1);
   1.373 -    val strT_name = Binding.name_of o strT_bind;
   1.374      val strT_def_bind = rpair [] o Thm.def_binding o strT_bind;
   1.375  
   1.376      fun strT_spec mapFT FT i =
   1.377        let
   1.378 -        val strTT = treeT --> FT;
   1.379 -
   1.380          fun mk_f i k k' =
   1.381            let val in_k = mk_InN sbdTs k i;
   1.382            in Term.absfree k' (HOLogic.mk_prod (mk_Shift Kl in_k, mk_shift lab in_k)) end;
   1.383 @@ -1167,25 +1131,24 @@
   1.384          val f = Term.list_comb (mapFT, passive_ids @ map3 mk_f ks kks kks');
   1.385          val (fTs1, fTs2) = apsnd tl (chop (i - 1) (map (fn T => T --> FT) bdFTs));
   1.386          val fs = map mk_undefined fTs1 @ (f :: map mk_undefined fTs2);
   1.387 -        val lhs = Free (strT_name i, strTT);
   1.388 -        val rhs = HOLogic.mk_split (Term.absfree Kl' (Term.absfree lab'
   1.389 -          (mk_sum_caseN fs $ (lab $ HOLogic.mk_list sum_sbdT []))));
   1.390        in
   1.391 -        mk_Trueprop_eq (lhs, rhs)
   1.392 +        HOLogic.mk_split (Term.absfree Kl' (Term.absfree lab'
   1.393 +          (mk_sum_caseN fs $ (lab $ HOLogic.mk_list sum_sbdT []))))
   1.394        end;
   1.395  
   1.396      val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) =
   1.397        lthy
   1.398 -      |> fold_map3 (fn i => fn mapFT => fn FT => Specification.definition
   1.399 -        (SOME (strT_bind i, NONE, NoSyn), (strT_def_bind i, strT_spec mapFT FT i)))
   1.400 +      |> fold_map3 (fn i => fn mapFT => fn FT => Local_Theory.define
   1.401 +        ((strT_bind i, NoSyn), (strT_def_bind i, strT_spec mapFT FT i)))
   1.402          ks tree_maps treeFTs
   1.403        |>> apsnd split_list o split_list
   1.404        ||> `Local_Theory.restore;
   1.405  
   1.406      val phi = Proof_Context.export_morphism lthy_old lthy;
   1.407  
   1.408 -    val strT_defs = map ((fn def => trans OF [def RS fun_cong, @{thm prod.cases}]) o
   1.409 -      Morphism.thm phi) strT_def_frees;
   1.410 +    val strT_defs = map (fn def =>
   1.411 +        trans OF [Morphism.thm phi def RS meta_eq_to_obj_eq RS fun_cong, @{thm prod.cases}])
   1.412 +      strT_def_frees;
   1.413      val strTs = map (fst o Term.dest_Const o Morphism.term phi) strT_frees;
   1.414  
   1.415      fun mk_strT FT i = Const (nth strTs (i - 1), treeT --> FT);
   1.416 @@ -1215,7 +1178,6 @@
   1.417      val from_to_sbd_thmss = mk_to_sbd_thmss @{thm fromCard_toCard};
   1.418  
   1.419      val Lev_bind = mk_internal_b LevN;
   1.420 -    val Lev_name = Binding.name_of Lev_bind;
   1.421      val Lev_def_bind = rpair [] (Thm.def_binding Lev_bind);
   1.422  
   1.423      val Lev_spec =
   1.424 @@ -1240,20 +1202,19 @@
   1.425          val Suc = Term.absdummy HOLogic.natT (Term.absfree Lev_rec'
   1.426            (HOLogic.mk_tuple (map5 mk_Suc ks ss setssAs zs zs')));
   1.427  
   1.428 -        val lhs = Term.list_comb (Free (Lev_name, LevT), ss);
   1.429          val rhs = mk_nat_rec Zero Suc;
   1.430        in
   1.431 -        mk_Trueprop_eq (lhs, rhs)
   1.432 +        fold_rev (Term.absfree o Term.dest_Free) ss rhs
   1.433        end;
   1.434  
   1.435      val ((Lev_free, (_, Lev_def_free)), (lthy, lthy_old)) =
   1.436        lthy
   1.437 -      |> Specification.definition (SOME (Lev_bind, NONE, NoSyn), (Lev_def_bind, Lev_spec))
   1.438 +      |> Local_Theory.define ((Lev_bind, NoSyn), (Lev_def_bind, Lev_spec))
   1.439        ||> `Local_Theory.restore;
   1.440  
   1.441      val phi = Proof_Context.export_morphism lthy_old lthy;
   1.442  
   1.443 -    val Lev_def = Morphism.thm phi Lev_def_free;
   1.444 +    val Lev_def = mk_unabs_def n (Morphism.thm phi Lev_def_free RS meta_eq_to_obj_eq);
   1.445      val Lev = fst (Term.dest_Const (Morphism.term phi Lev_free));
   1.446  
   1.447      fun mk_Lev ss nat i =
   1.448 @@ -1269,7 +1230,6 @@
   1.449      val Lev_Sucs = flat (mk_rec_simps n @{thm nat_rec_Suc_imp} [Lev_def]);
   1.450  
   1.451      val rv_bind = mk_internal_b rvN;
   1.452 -    val rv_name = Binding.name_of rv_bind;
   1.453      val rv_def_bind = rpair [] (Thm.def_binding rv_bind);
   1.454  
   1.455      val rv_spec =
   1.456 @@ -1285,20 +1245,19 @@
   1.457          val Cons = Term.absfree sumx' (Term.absdummy sum_sbd_listT (Term.absfree rv_rec'
   1.458            (HOLogic.mk_tuple (map4 mk_Cons ks ss zs zs'))));
   1.459  
   1.460 -        val lhs = Term.list_comb (Free (rv_name, rvT), ss);
   1.461          val rhs = mk_list_rec Nil Cons;
   1.462        in
   1.463 -        mk_Trueprop_eq (lhs, rhs)
   1.464 +        fold_rev (Term.absfree o Term.dest_Free) ss rhs
   1.465        end;
   1.466  
   1.467      val ((rv_free, (_, rv_def_free)), (lthy, lthy_old)) =
   1.468        lthy
   1.469 -      |> Specification.definition (SOME (rv_bind, NONE, NoSyn), (rv_def_bind, rv_spec))
   1.470 +      |> Local_Theory.define ((rv_bind, NoSyn), (rv_def_bind, rv_spec))
   1.471        ||> `Local_Theory.restore;
   1.472  
   1.473      val phi = Proof_Context.export_morphism lthy_old lthy;
   1.474  
   1.475 -    val rv_def = Morphism.thm phi rv_def_free;
   1.476 +    val rv_def = mk_unabs_def n (Morphism.thm phi rv_def_free RS meta_eq_to_obj_eq);
   1.477      val rv = fst (Term.dest_Const (Morphism.term phi rv_free));
   1.478  
   1.479      fun mk_rv ss kl i =
   1.480 @@ -1316,13 +1275,10 @@
   1.481  
   1.482      val beh_binds = mk_internal_bs behN;
   1.483      fun beh_bind i = nth beh_binds (i - 1);
   1.484 -    val beh_name = Binding.name_of o beh_bind;
   1.485      val beh_def_bind = rpair [] o Thm.def_binding o beh_bind;
   1.486  
   1.487      fun beh_spec i z =
   1.488        let
   1.489 -        val mk_behT = Library.foldr (op -->) (map fastype_of (ss @ [z]), treeT);
   1.490 -
   1.491          fun mk_case i to_sbd_map s k k' =
   1.492            Term.absfree k' (mk_InN bdFTs
   1.493              (Term.list_comb (to_sbd_map, passive_ids @ map (mk_to_sbd s k i) ks) $ (s $ k)) i);
   1.494 @@ -1332,23 +1288,23 @@
   1.495            (mk_sum_caseN (map5 mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z))
   1.496            (mk_undefined sbdFT));
   1.497  
   1.498 -        val lhs = Term.list_comb (Free (beh_name i, mk_behT), ss) $ z;
   1.499          val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
   1.500            (Term.absfree nat' (mk_Lev ss nat i $ z)), Lab);
   1.501        in
   1.502 -        mk_Trueprop_eq (lhs, rhs)
   1.503 +        fold_rev (Term.absfree o Term.dest_Free) (ss @ [z]) rhs
   1.504        end;
   1.505  
   1.506      val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) =
   1.507        lthy
   1.508 -      |> fold_map2 (fn i => fn z => Specification.definition
   1.509 -        (SOME (beh_bind i, NONE, NoSyn), (beh_def_bind i, beh_spec i z))) ks zs
   1.510 +      |> fold_map2 (fn i => fn z =>
   1.511 +        Local_Theory.define ((beh_bind i, NoSyn), (beh_def_bind i, beh_spec i z))) ks zs
   1.512        |>> apsnd split_list o split_list
   1.513        ||> `Local_Theory.restore;
   1.514  
   1.515      val phi = Proof_Context.export_morphism lthy_old lthy;
   1.516  
   1.517 -    val beh_defs = map (Morphism.thm phi) beh_def_frees;
   1.518 +    val beh_defs = map (fn def =>
   1.519 +      mk_unabs_def (n + 1) (Morphism.thm phi def RS meta_eq_to_obj_eq)) beh_def_frees;
   1.520      val behs = map (fst o Term.dest_Const o Morphism.term phi) beh_frees;
   1.521  
   1.522      fun mk_beh ss i =
   1.523 @@ -1651,8 +1607,6 @@
   1.524        mk_map_of_bnf Ds (passiveAs @ prodTs) (passiveAs @ Ts)) Dss bnfs;
   1.525      val fstsTs = map fst_const prodTs;
   1.526      val sndsTs = map snd_const prodTs;
   1.527 -    val dtorTs = map2 (curry op -->) Ts FTs;
   1.528 -    val ctorTs = map2 (curry op -->) FTs Ts;
   1.529      val unfold_fTs = map2 (curry op -->) activeAs Ts;
   1.530      val corec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) sum_sTs;
   1.531      val corec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls;
   1.532 @@ -1677,25 +1631,18 @@
   1.533        ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs);
   1.534  
   1.535      fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
   1.536 -    val dtor_name = Binding.name_of o dtor_bind;
   1.537      val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
   1.538  
   1.539 -    fun dtor_spec i rep str map_FT dtorT Jz Jz' =
   1.540 -      let
   1.541 -        val lhs = Free (dtor_name i, dtorT);
   1.542 -        val rhs = Term.absfree Jz'
   1.543 -          (Term.list_comb (map_FT, map HOLogic.id_const passiveAs @ Abs_Ts) $
   1.544 -            (str $ (rep $ Jz)));
   1.545 -      in
   1.546 -        mk_Trueprop_eq (lhs, rhs)
   1.547 -      end;
   1.548 +    fun dtor_spec rep str map_FT Jz Jz' =
   1.549 +      Term.absfree Jz'
   1.550 +        (Term.list_comb (map_FT, map HOLogic.id_const passiveAs @ Abs_Ts) $ (str $ (rep $ Jz)));
   1.551  
   1.552      val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
   1.553        lthy
   1.554 -      |> fold_map7 (fn i => fn rep => fn str => fn mapx => fn dtorT => fn Jz => fn Jz' =>
   1.555 -        Specification.definition (SOME (dtor_bind i, NONE, NoSyn),
   1.556 -          (dtor_def_bind i, dtor_spec i rep str mapx dtorT Jz Jz')))
   1.557 -        ks Rep_Ts str_finals map_FTs dtorTs Jzs Jzs'
   1.558 +      |> fold_map6 (fn i => fn rep => fn str => fn mapx => fn Jz => fn Jz' =>
   1.559 +        Local_Theory.define ((dtor_bind i, NoSyn),
   1.560 +          (dtor_def_bind i, dtor_spec rep str mapx Jz Jz')))
   1.561 +        ks Rep_Ts str_finals map_FTs Jzs Jzs'
   1.562        |>> apsnd split_list o split_list
   1.563        ||> `Local_Theory.restore;
   1.564  
   1.565 @@ -1705,7 +1652,8 @@
   1.566          Morphism.term phi) dtor_frees;
   1.567      val dtors = mk_dtors passiveAs;
   1.568      val dtor's = mk_dtors passiveBs;
   1.569 -    val dtor_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) dtor_def_frees;
   1.570 +    val dtor_defs = map (fn def =>
   1.571 +      Morphism.thm phi def RS meta_eq_to_obj_eq RS fun_cong) dtor_def_frees;
   1.572  
   1.573      val coalg_final_set_thmss = map (map (fn thm => coalg_final_thm RS thm)) coalg_set_thmss;
   1.574      val (mor_Rep_thm, mor_Abs_thm) =
   1.575 @@ -1730,26 +1678,16 @@
   1.576      val timer = time (timer "dtor definitions & thms");
   1.577  
   1.578      fun unfold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_unfoldN ^ "_");
   1.579 -    val unfold_name = Binding.name_of o unfold_bind;
   1.580      val unfold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o unfold_bind;
   1.581  
   1.582 -    fun unfold_spec i T AT abs f z z' =
   1.583 -      let
   1.584 -        val unfoldT = Library.foldr (op -->) (sTs, AT --> T);
   1.585 -
   1.586 -        val lhs = Term.list_comb (Free (unfold_name i, unfoldT), ss);
   1.587 -        val rhs = Term.absfree z' (abs $ (f $ z));
   1.588 -      in
   1.589 -        mk_Trueprop_eq (lhs, rhs)
   1.590 -      end;
   1.591 +    fun unfold_spec abs f z = fold_rev (Term.absfree o Term.dest_Free) (ss @ [z]) (abs $ (f $ z));
   1.592  
   1.593      val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) =
   1.594        lthy
   1.595 -      |> fold_map7 (fn i => fn T => fn AT => fn abs => fn f => fn z => fn z' =>
   1.596 -        Specification.definition
   1.597 -          (SOME (unfold_bind i, NONE, NoSyn), (unfold_def_bind i, unfold_spec i T AT abs f z z')))
   1.598 -          ks Ts activeAs Abs_Ts (map (fn i => HOLogic.mk_comp
   1.599 -            (mk_proj (mk_LSBIS passive_UNIVs i), mk_beh ss i)) ks) zs zs'
   1.600 +      |> fold_map4 (fn i => fn abs => fn f => fn z =>
   1.601 +        Local_Theory.define ((unfold_bind i, NoSyn), (unfold_def_bind i, unfold_spec abs f z)))
   1.602 +          ks Abs_Ts (map (fn i => HOLogic.mk_comp
   1.603 +            (mk_proj (mk_LSBIS passive_UNIVs i), mk_beh ss i)) ks) zs
   1.604        |>> apsnd split_list o split_list
   1.605        ||> `Local_Theory.restore;
   1.606  
   1.607 @@ -1763,7 +1701,8 @@
   1.608        unfold_names (mk_Ts passives) actives;
   1.609      fun mk_unfold Ts ss i = Term.list_comb (Const (nth unfold_names (i - 1), Library.foldr (op -->)
   1.610        (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
   1.611 -    val unfold_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) unfold_def_frees;
   1.612 +    val unfold_defs = map (fn def =>
   1.613 +      mk_unabs_def (n + 1) (Morphism.thm phi def RS meta_eq_to_obj_eq)) unfold_def_frees;
   1.614  
   1.615      val mor_unfold_thm =
   1.616        let
   1.617 @@ -1832,22 +1771,14 @@
   1.618          map HOLogic.id_const passiveAs @ dtors)) Dss bnfs;
   1.619  
   1.620      fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
   1.621 -    val ctor_name = Binding.name_of o ctor_bind;
   1.622      val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
   1.623  
   1.624 -    fun ctor_spec i ctorT =
   1.625 -      let
   1.626 -        val lhs = Free (ctor_name i, ctorT);
   1.627 -        val rhs = mk_unfold Ts map_dtors i;
   1.628 -      in
   1.629 -        mk_Trueprop_eq (lhs, rhs)
   1.630 -      end;
   1.631 +    fun ctor_spec i = mk_unfold Ts map_dtors i;
   1.632  
   1.633      val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
   1.634        lthy
   1.635 -      |> fold_map2 (fn i => fn ctorT =>
   1.636 -        Specification.definition
   1.637 -          (SOME (ctor_bind i, NONE, NoSyn), (ctor_def_bind i, ctor_spec i ctorT))) ks ctorTs
   1.638 +      |> fold_map (fn i =>
   1.639 +        Local_Theory.define ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec i))) ks
   1.640        |>> apsnd split_list o split_list
   1.641        ||> `Local_Theory.restore;
   1.642  
   1.643 @@ -1856,7 +1787,7 @@
   1.644        map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi)
   1.645          ctor_frees;
   1.646      val ctors = mk_ctors params';
   1.647 -    val ctor_defs = map (Morphism.thm phi) ctor_def_frees;
   1.648 +    val ctor_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) ctor_def_frees;
   1.649  
   1.650      val ctor_o_dtor_thms = map2 (fold_thms lthy o single) ctor_defs unfold_o_dtor_thms;
   1.651  
   1.652 @@ -1904,7 +1835,6 @@
   1.653        end;
   1.654  
   1.655      fun corec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_corecN ^ "_");
   1.656 -    val corec_name = Binding.name_of o corec_bind;
   1.657      val corec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o corec_bind;
   1.658  
   1.659      val corec_strs =
   1.660 @@ -1914,20 +1844,13 @@
   1.661        dtors corec_ss corec_maps;
   1.662  
   1.663      fun corec_spec i T AT =
   1.664 -      let
   1.665 -        val corecT = Library.foldr (op -->) (corec_sTs, AT --> T);
   1.666 -
   1.667 -        val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss);
   1.668 -        val rhs = HOLogic.mk_comp (mk_unfold Ts corec_strs i, Inr_const T AT);
   1.669 -      in
   1.670 -        mk_Trueprop_eq (lhs, rhs)
   1.671 -      end;
   1.672 +      fold_rev (Term.absfree o Term.dest_Free) corec_ss
   1.673 +        (HOLogic.mk_comp (mk_unfold Ts corec_strs i, Inr_const T AT));
   1.674  
   1.675      val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) =
   1.676        lthy
   1.677        |> fold_map3 (fn i => fn T => fn AT =>
   1.678 -        Specification.definition
   1.679 -          (SOME (corec_bind i, NONE, NoSyn), (corec_def_bind i, corec_spec i T AT)))
   1.680 +        Local_Theory.define ((corec_bind i, NoSyn), (corec_def_bind i, corec_spec i T AT)))
   1.681            ks Ts activeAs
   1.682        |>> apsnd split_list o split_list
   1.683        ||> `Local_Theory.restore;
   1.684 @@ -1937,7 +1860,8 @@
   1.685      val corec_names = map (fst o dest_Const) corecs;
   1.686      fun mk_corec ss i = Term.list_comb (Const (nth corec_names (i - 1), Library.foldr (op -->)
   1.687        (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
   1.688 -    val corec_defs = map (Morphism.thm phi) corec_def_frees;
   1.689 +    val corec_defs = map (fn def =>
   1.690 +      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) corec_def_frees;
   1.691  
   1.692      val sum_cases =
   1.693        map2 (fn T => fn i => mk_sum_case (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks;
     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Fri Jan 31 13:42:47 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Fri Jan 31 13:45:39 2014 +0100
     2.3 @@ -244,32 +244,28 @@
     2.4      (* algebra *)
     2.5  
     2.6      val alg_bind = mk_internal_b algN;
     2.7 -    val alg_name = Binding.name_of alg_bind;
     2.8      val alg_def_bind = (Thm.def_binding alg_bind, []);
     2.9  
    2.10      (*forall i = 1 ... n: (\<forall>x \<in> Fi_in A1 .. Am B1 ... Bn. si x \<in> Bi)*)
    2.11      val alg_spec =
    2.12        let
    2.13 -        val algT = Library.foldr (op -->) (ATs @ BTs @ sTs, HOLogic.boolT);
    2.14 -
    2.15          val ins = map3 mk_in (replicate n (As @ Bs)) setssAs FTsAs;
    2.16          fun mk_alg_conjunct B s X x x' =
    2.17            mk_Ball X (Term.absfree x' (HOLogic.mk_mem (s $ x, B)));
    2.18  
    2.19 -        val lhs = Term.list_comb (Free (alg_name, algT), As @ Bs @ ss);
    2.20          val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_alg_conjunct Bs ss ins xFs xFs')
    2.21        in
    2.22 -        mk_Trueprop_eq (lhs, rhs)
    2.23 +        fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss) rhs
    2.24        end;
    2.25  
    2.26      val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
    2.27          lthy
    2.28 -        |> Specification.definition (SOME (alg_bind, NONE, NoSyn), (alg_def_bind, alg_spec))
    2.29 +        |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec))
    2.30          ||> `Local_Theory.restore;
    2.31  
    2.32      val phi = Proof_Context.export_morphism lthy_old lthy;
    2.33      val alg = fst (Term.dest_Const (Morphism.term phi alg_free));
    2.34 -    val alg_def = Morphism.thm phi alg_def_free;
    2.35 +    val alg_def = mk_unabs_def (live + n) (Morphism.thm phi alg_def_free RS meta_eq_to_obj_eq);
    2.36  
    2.37      fun mk_alg As Bs ss =
    2.38        let
    2.39 @@ -331,7 +327,6 @@
    2.40      (* morphism *)
    2.41  
    2.42      val mor_bind = mk_internal_b morN;
    2.43 -    val mor_name = Binding.name_of mor_bind;
    2.44      val mor_def_bind = (Thm.def_binding mor_bind, []);
    2.45  
    2.46      (*fbetw) forall i = 1 ... n: (\<forall>x \<in> Bi. f x \<in> B'i)*)
    2.47 @@ -339,31 +334,28 @@
    2.48         f (s1 x) = s1' (Fi_map id ... id f1 ... fn x))*)
    2.49      val mor_spec =
    2.50        let
    2.51 -        val morT = Library.foldr (op -->) (BTs @ sTs @ B'Ts @ s'Ts @ fTs, HOLogic.boolT);
    2.52 -
    2.53          fun mk_fbetw f B1 B2 z z' =
    2.54            mk_Ball B1 (Term.absfree z' (HOLogic.mk_mem (f $ z, B2)));
    2.55          fun mk_mor sets mapAsBs f s s' T x x' =
    2.56            mk_Ball (mk_in (passive_UNIVs @ Bs) sets T)
    2.57              (Term.absfree x' (HOLogic.mk_eq (f $ (s $ x), s' $
    2.58                (Term.list_comb (mapAsBs, passive_ids @ fs) $ x))));
    2.59 -        val lhs = Term.list_comb (Free (mor_name, morT), Bs @ ss @ B's @ s's @ fs);
    2.60          val rhs = HOLogic.mk_conj
    2.61            (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'),
    2.62            Library.foldr1 HOLogic.mk_conj
    2.63              (map8 mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs'))
    2.64        in
    2.65 -        mk_Trueprop_eq (lhs, rhs)
    2.66 +        fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs
    2.67        end;
    2.68  
    2.69      val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
    2.70          lthy
    2.71 -        |> Specification.definition (SOME (mor_bind, NONE, NoSyn), (mor_def_bind, mor_spec))
    2.72 +        |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
    2.73          ||> `Local_Theory.restore;
    2.74  
    2.75      val phi = Proof_Context.export_morphism lthy_old lthy;
    2.76      val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
    2.77 -    val mor_def = Morphism.thm phi mor_def_free;
    2.78 +    val mor_def = mk_unabs_def (5 * n) (Morphism.thm phi mor_def_free RS meta_eq_to_obj_eq);
    2.79  
    2.80      fun mk_mor Bs1 ss1 Bs2 ss2 fs =
    2.81        let
    2.82 @@ -719,31 +711,27 @@
    2.83  
    2.84      val min_alg_binds = mk_internal_bs min_algN;
    2.85      fun min_alg_bind i = nth min_alg_binds (i - 1);
    2.86 -    fun min_alg_name i = Binding.name_of (min_alg_bind i);
    2.87      val min_alg_def_bind = rpair [] o Thm.def_binding o min_alg_bind;
    2.88  
    2.89      fun min_alg_spec i =
    2.90        let
    2.91 -        val min_algT =
    2.92 -          Library.foldr (op -->) (ATs @ sTs, HOLogic.mk_setT (nth activeAs (i - 1)));
    2.93 -
    2.94 -        val lhs = Term.list_comb (Free (min_alg_name i, min_algT), As @ ss);
    2.95          val rhs = mk_UNION (field_suc_bd)
    2.96            (Term.absfree idx' (mk_nthN n (mk_min_algs As ss $ idx) i));
    2.97        in
    2.98 -        mk_Trueprop_eq (lhs, rhs)
    2.99 +        fold_rev (Term.absfree o Term.dest_Free) (As @ ss) rhs
   2.100        end;
   2.101  
   2.102      val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
   2.103          lthy
   2.104 -        |> fold_map (fn i => Specification.definition
   2.105 -          (SOME (min_alg_bind i, NONE, NoSyn), (min_alg_def_bind i, min_alg_spec i))) ks
   2.106 +        |> fold_map (fn i => Local_Theory.define
   2.107 +          ((min_alg_bind i, NoSyn), (min_alg_def_bind i, min_alg_spec i))) ks
   2.108          |>> apsnd split_list o split_list
   2.109          ||> `Local_Theory.restore;
   2.110  
   2.111      val phi = Proof_Context.export_morphism lthy_old lthy;
   2.112      val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees;
   2.113 -    val min_alg_defs = map (Morphism.thm phi) min_alg_def_frees;
   2.114 +    val min_alg_defs = map (fn def =>
   2.115 +      mk_unabs_def live (Morphism.thm phi def RS meta_eq_to_obj_eq)) min_alg_def_frees;
   2.116  
   2.117      fun mk_min_alg As ss i =
   2.118        let
   2.119 @@ -832,30 +820,25 @@
   2.120  
   2.121      val str_init_binds = mk_internal_bs str_initN;
   2.122      fun str_init_bind i = nth str_init_binds (i - 1);
   2.123 -    val str_init_name = Binding.name_of o str_init_bind;
   2.124      val str_init_def_bind = rpair [] o Thm.def_binding o str_init_bind;
   2.125  
   2.126      fun str_init_spec i =
   2.127        let
   2.128 -        val T = nth init_FTs (i - 1);
   2.129          val init_xF = nth init_xFs (i - 1)
   2.130          val select_s = nth select_ss (i - 1);
   2.131          val map = mk_map_of_bnf (nth Dss (i - 1))
   2.132            (passiveAs @ active_initTs) (passiveAs @ replicate n Asuc_bdT)
   2.133            (nth bnfs (i - 1));
   2.134          val map_args = passive_ids @ replicate n (mk_rapp iidx Asuc_bdT);
   2.135 -        val str_initT = T --> IIT --> Asuc_bdT;
   2.136 -
   2.137 -        val lhs = Term.list_comb (Free (str_init_name i, str_initT), [init_xF, iidx]);
   2.138          val rhs = select_s $ (Term.list_comb (map, map_args) $ init_xF);
   2.139        in
   2.140 -        mk_Trueprop_eq (lhs, rhs)
   2.141 +        fold_rev (Term.absfree o Term.dest_Free) [init_xF, iidx] rhs
   2.142        end;
   2.143  
   2.144      val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) =
   2.145        lthy
   2.146 -      |> fold_map (fn i => Specification.definition
   2.147 -        (SOME (str_init_bind i, NONE, NoSyn), (str_init_def_bind i, str_init_spec i))) ks
   2.148 +      |> fold_map (fn i => Local_Theory.define
   2.149 +        ((str_init_bind i, NoSyn), (str_init_def_bind i, str_init_spec i))) ks
   2.150        |>> apsnd split_list o split_list
   2.151        ||> `Local_Theory.restore;
   2.152  
   2.153 @@ -864,7 +847,8 @@
   2.154        map (Term.subst_atomic_types (map (`(Morphism.typ phi)) params') o Morphism.term phi)
   2.155          str_init_frees;
   2.156  
   2.157 -    val str_init_defs = map (Morphism.thm phi) str_init_def_frees;
   2.158 +    val str_init_defs = map (fn def =>
   2.159 +      mk_unabs_def 2 (Morphism.thm phi def RS meta_eq_to_obj_eq)) str_init_def_frees;
   2.160  
   2.161      val car_inits = map (mk_min_alg passive_UNIVs str_inits) ks;
   2.162  
   2.163 @@ -1024,25 +1008,17 @@
   2.164      val phi2s = map2 retype_free (map2 mk_pred2T Ts Ts') init_phis;
   2.165  
   2.166      fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
   2.167 -    val ctor_name = Binding.name_of o ctor_bind;
   2.168      val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
   2.169  
   2.170 -    fun ctor_spec i abs str map_FT_init x x' =
   2.171 -      let
   2.172 -        val ctorT = nth FTs (i - 1) --> nth Ts (i - 1);
   2.173 -
   2.174 -        val lhs = Free (ctor_name i, ctorT);
   2.175 -        val rhs = Term.absfree x' (abs $ (str $
   2.176 +    fun ctor_spec abs str map_FT_init x x' =
   2.177 +      Term.absfree x' (abs $ (str $
   2.178            (Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts) $ x)));
   2.179 -      in
   2.180 -        mk_Trueprop_eq (lhs, rhs)
   2.181 -      end;
   2.182  
   2.183      val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
   2.184        lthy
   2.185        |> fold_map6 (fn i => fn abs => fn str => fn mapx => fn x => fn x' =>
   2.186 -        Specification.definition
   2.187 -          (SOME (ctor_bind i, NONE, NoSyn), (ctor_def_bind i, ctor_spec i abs str mapx x x')))
   2.188 +        Local_Theory.define
   2.189 +          ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec abs str mapx x x')))
   2.190            ks Abs_Ts str_inits map_FT_inits xFs xFs'
   2.191        |>> apsnd split_list o split_list
   2.192        ||> `Local_Theory.restore;
   2.193 @@ -1053,7 +1029,7 @@
   2.194          Morphism.term phi) ctor_frees;
   2.195      val ctors = mk_ctors passiveAs;
   2.196      val ctor's = mk_ctors passiveBs;
   2.197 -    val ctor_defs = map (Morphism.thm phi) ctor_def_frees;
   2.198 +    val ctor_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) ctor_def_frees;
   2.199  
   2.200      val (mor_Rep_thm, mor_Abs_thm) =
   2.201        let
   2.202 @@ -1084,25 +1060,14 @@
   2.203      val foldx = HOLogic.choice_const foldT $ fold_fun;
   2.204  
   2.205      fun fold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_foldN ^ "_");
   2.206 -    val fold_name = Binding.name_of o fold_bind;
   2.207      val fold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o fold_bind;
   2.208  
   2.209 -    fun fold_spec i T AT =
   2.210 -      let
   2.211 -        val foldT = Library.foldr (op -->) (sTs, T --> AT);
   2.212 -
   2.213 -        val lhs = Term.list_comb (Free (fold_name i, foldT), ss);
   2.214 -        val rhs = mk_nthN n foldx i;
   2.215 -      in
   2.216 -        mk_Trueprop_eq (lhs, rhs)
   2.217 -      end;
   2.218 +    fun fold_spec i = fold_rev (Term.absfree o Term.dest_Free) ss (mk_nthN n foldx i);
   2.219  
   2.220      val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) =
   2.221        lthy
   2.222 -      |> fold_map3 (fn i => fn T => fn AT =>
   2.223 -        Specification.definition
   2.224 -          (SOME (fold_bind i, NONE, NoSyn), (fold_def_bind i, fold_spec i T AT)))
   2.225 -          ks Ts activeAs
   2.226 +      |> fold_map (fn i =>
   2.227 +        Local_Theory.define ((fold_bind i, NoSyn), (fold_def_bind i, fold_spec i))) ks
   2.228        |>> apsnd split_list o split_list
   2.229        ||> `Local_Theory.restore;
   2.230  
   2.231 @@ -1116,7 +1081,8 @@
   2.232        fold_names (mk_Ts passives) actives;
   2.233      fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->)
   2.234        (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
   2.235 -    val fold_defs = map (Morphism.thm phi) fold_def_frees;
   2.236 +    val fold_defs = map (fn def =>
   2.237 +      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) fold_def_frees;
   2.238  
   2.239      val mor_fold_thm =
   2.240        let
   2.241 @@ -1174,24 +1140,14 @@
   2.242          map HOLogic.id_const passiveAs @ ctors)) Dss bnfs;
   2.243  
   2.244      fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
   2.245 -    val dtor_name = Binding.name_of o dtor_bind;
   2.246      val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
   2.247  
   2.248 -    fun dtor_spec i FT T =
   2.249 -      let
   2.250 -        val dtorT = T --> FT;
   2.251 -
   2.252 -        val lhs = Free (dtor_name i, dtorT);
   2.253 -        val rhs = mk_fold Ts map_ctors i;
   2.254 -      in
   2.255 -        mk_Trueprop_eq (lhs, rhs)
   2.256 -      end;
   2.257 +    fun dtor_spec i = mk_fold Ts map_ctors i;
   2.258  
   2.259      val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
   2.260        lthy
   2.261 -      |> fold_map3 (fn i => fn FT => fn T =>
   2.262 -        Specification.definition
   2.263 -          (SOME (dtor_bind i, NONE, NoSyn), (dtor_def_bind i, dtor_spec i FT T))) ks FTs Ts
   2.264 +      |> fold_map (fn i =>
   2.265 +        Local_Theory.define ((dtor_bind i, NoSyn), (dtor_def_bind i, dtor_spec i))) ks
   2.266        |>> apsnd split_list o split_list
   2.267        ||> `Local_Theory.restore;
   2.268  
   2.269 @@ -1200,7 +1156,7 @@
   2.270        map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi)
   2.271          dtor_frees;
   2.272      val dtors = mk_dtors params';
   2.273 -    val dtor_defs = map (Morphism.thm phi) dtor_def_frees;
   2.274 +    val dtor_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) dtor_def_frees;
   2.275  
   2.276      val ctor_o_dtor_thms = map2 (fold_thms lthy o single) dtor_defs ctor_o_fold_thms;
   2.277  
   2.278 @@ -1247,7 +1203,6 @@
   2.279        end;
   2.280  
   2.281      fun rec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_recN ^ "_");
   2.282 -    val rec_name = Binding.name_of o rec_bind;
   2.283      val rec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o rec_bind;
   2.284  
   2.285      val rec_strs =
   2.286 @@ -1256,21 +1211,13 @@
   2.287        ctors rec_ss rec_maps;
   2.288  
   2.289      fun rec_spec i T AT =
   2.290 -      let
   2.291 -        val recT = Library.foldr (op -->) (rec_sTs, T --> AT);
   2.292 -
   2.293 -        val lhs = Term.list_comb (Free (rec_name i, recT), rec_ss);
   2.294 -        val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts rec_strs i);
   2.295 -      in
   2.296 -        mk_Trueprop_eq (lhs, rhs)
   2.297 -      end;
   2.298 +      fold_rev (Term.absfree o Term.dest_Free) rec_ss
   2.299 +        (HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts rec_strs i));
   2.300  
   2.301      val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) =
   2.302        lthy
   2.303        |> fold_map3 (fn i => fn T => fn AT =>
   2.304 -        Specification.definition
   2.305 -          (SOME (rec_bind i, NONE, NoSyn), (rec_def_bind i, rec_spec i T AT)))
   2.306 -          ks Ts activeAs
   2.307 +        Local_Theory.define ((rec_bind i, NoSyn), (rec_def_bind i, rec_spec i T AT))) ks Ts activeAs
   2.308        |>> apsnd split_list o split_list
   2.309        ||> `Local_Theory.restore;
   2.310  
   2.311 @@ -1279,7 +1226,8 @@
   2.312      val rec_names = map (fst o dest_Const) recs;
   2.313      fun mk_rec ss i = Term.list_comb (Const (nth rec_names (i - 1), Library.foldr (op -->)
   2.314        (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
   2.315 -    val rec_defs = map (Morphism.thm phi) rec_def_frees;
   2.316 +    val rec_defs = map (fn def =>
   2.317 +      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) rec_def_frees;
   2.318  
   2.319      val convols = map2 (fn T => fn i => mk_convol (HOLogic.id_const T, mk_rec rec_ss i)) Ts ks;
   2.320      val ctor_rec_thms =