Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/NewFv.thy
changeset 2288 3b83960f9544
parent 2163 5dc48e1af733
child 2312 ad03df7e8056
equal deleted inserted replaced
2164:a5dc3558cdec 2288:3b83960f9544 
     2 imports "../Nominal-General/Nominal2_Atoms"
 
     2 imports "../Nominal-General/Nominal2_Atoms"
 
     3         "Abs" "Perm" "Nominal2_FSet"
 
     3         "Abs" "Perm" "Nominal2_FSet"
 
     4 begin
 
     4 begin
 
     5 
     5 
     6 ML {*
 
     6 ML {*
 
     7 (* binding modes *)
 
     7 (* binding modes  and binding clauses *)
 
     8 
     8 
     9 datatype bmodes =
 
     9 datatype bmode = Lst | Res | Set
 
    10    BEmy of int
 
    10 
    11 |  BLst of ((term option * int) list) * (int list)
 
    11 datatype bclause =
 
    12 |  BSet of ((term option * int) list) * (int list)
 
    12   BC of bmode * (term option * int) list * int list
 
    13 |  BRes of ((term option * int) list) * (int list)
 
    13 *}
 
    14 *}
 
    14 
    15 
    15 ML {*
 
    16 ML {*
 
    16 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}
 
    17 fun mk_singleton_atom x = HOLogic.mk_set @{typ atom} [mk_atom x];
 
    17   | mk_diff (t1, @{term "{}::atom set"}) = t1
 
    18 
    18   | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)
 
    19 val noatoms = @{term "{} :: atom set"};
 
    19 
    20 
    20 fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"}
 
    21 fun mk_union sets =
 
    21   | mk_union (t1 , @{term "{}::atom set"}) = t1
 
    22   fold (fn a => fn b =>
 
    22   | mk_union (@{term "{}::atom set"}, t2) = t2
 
    23   if a = noatoms then b else
 
    23   | mk_union (t1, t2) = HOLogic.mk_binop @{const_name sup} (t1, t2)  
    24   if b = noatoms then a else
 
    24  
    25   if a = b then a else
 
    25 fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"}
 
    26   HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
 
    26 *}
 
    27 *}
 
    27 
    28 
    28 ML {*
 
    29 ML {*
 
    29 fun is_atom ctxt ty =
 
    30 fun is_atom thy ty =
 
    30   Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
 
    31   Sign.of_sort thy (ty, @{sort at_base})
 
    31 
    32 
    32 fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
 
    33 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
 
       
    34   | is_atom_set _ _ = false;
 
    33   | is_atom_set _ _ = false;
 
    35 
    34 
    36 fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t
 
    35 fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
 
    37   | is_atom_fset _ _ = false;
 
    36   | is_atom_fset _ _ = false;
 
    38 
    37 
       
    38 fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
 
       
    39   | is_atom_list _ _ = false
 
       
    40 *}
 
       
    41 
       
    42 ML {*
 
    39 fun mk_atom_set t =
 
    43 fun mk_atom_set t =
 
    40 let
 
    44 let
 
    41   val ty = fastype_of t;
 
    45   val ty = fastype_of t;
 
    42   val atom_ty = HOLogic.dest_setT ty --> @{typ atom};
 
    46   val atom_ty = HOLogic.dest_setT ty --> @{typ atom};
 
    43   val img_ty = atom_ty --> ty --> @{typ "atom set"};
 
    47   val img_ty = atom_ty --> ty --> @{typ "atom set"};
 
    53   val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"}
 
    57   val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"}
 
    54 in
 
    58 in
 
    55   fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
 
    59   fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
 
    56 end;
 
    60 end;
 
    57 
    61 
    58 fun mk_diff a b =
 
       
    59   if b = noatoms then a else
 
       
    60   if b = a then noatoms else
 
       
    61   HOLogic.mk_binop @{const_name minus} (a, b);
 
       
    62 *}
 
       
    63 
       
    64 ML {*
 
       
    65 fun is_atom_list (Type (@{type_name list}, [T])) = true
 
       
    66   | is_atom_list _ = false
 
       
    67 *}
 
       
    68 
       
    69 ML {*
 
       
    70 fun dest_listT (Type (@{type_name list}, [T])) = T
 
       
    71   | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
 
       
    72 *}
 
       
    73 
       
    74 ML {*
 
       
    75 fun mk_atom_list t =
 
    62 fun mk_atom_list t =
 
    76 let
 
    63 let
 
    77   val ty = fastype_of t;
 
    64   val ty = fastype_of t;
 
    78   val atom_ty = dest_listT ty --> @{typ atom};
 
    65   val atom_ty = dest_listT ty --> @{typ atom};
 
    79   val map_ty = atom_ty --> ty --> @{typ "atom list"};
 
    66   val map_ty = atom_ty --> ty --> @{typ "atom list"};
 
    81   (Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t)
 
    68   (Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t)
 
    82 end;
 
    69 end;
 
    83 *}
 
    70 *}
 
    84 
    71 
    85 ML {*
 
    72 ML {*
 
    86 fun setify thy t =
 
    73 fun setify ctxt t =
 
    87 let
 
    74 let
 
    88   val ty = fastype_of t;
 
    75   val ty = fastype_of t;
 
    89 in
 
    76 in
 
    90   if is_atom thy ty
 
    77   if is_atom ctxt ty
 
    91     then mk_singleton_atom t
 
    78     then  HOLogic.mk_set @{typ atom} [mk_atom t]
 
    92   else if is_atom_set thy ty
 
    79   else if is_atom_set ctxt ty
 
    93     then mk_atom_set t
 
    80     then mk_atom_set t
 
    94   else if is_atom_fset thy ty
 
    81   else if is_atom_fset ctxt ty
 
    95     then mk_atom_fset t
 
    82     then mk_atom_fset t
 
    96   else error ("setify" ^ (PolyML.makestring (t, ty)))
 
    83   else error ("setify" ^ (PolyML.makestring (t, ty)))
 
    97 end
 
    84 end
 
    98 *}
 
    85 *}
 
    99 
    86 
   100 ML {*
 
    87 ML {*
 
   101 fun listify thy t =
 
    88 fun listify ctxt t =
 
   102 let
 
    89 let
 
   103   val ty = fastype_of t;
 
    90   val ty = fastype_of t;
 
   104 in
 
    91 in
 
   105   if is_atom thy ty
 
    92   if is_atom ctxt ty
 
   106     then HOLogic.mk_list @{typ atom} [mk_atom t]
 
    93     then HOLogic.mk_list @{typ atom} [mk_atom t]
 
   107   else if is_atom_list ty
 
    94   else if is_atom_list ctxt ty
 
   108     then mk_atom_set t
 
    95     then mk_atom_set t
 
   109   else error "listify"
 
    96   else error "listify"
 
   110 end
 
    97 end
 
   111 *}
 
    98 *}
 
   112 
    99 
   113 ML {*
 
   100 ML {*
 
   114 fun set x =
 
   101 fun to_set x =
 
   115   if fastype_of x = @{typ "atom list"}
 
   102   if fastype_of x = @{typ "atom list"}
 
   116   then @{term "set::atom list \<Rightarrow> atom set"} $ x
 
   103   then @{term "set::atom list \<Rightarrow> atom set"} $ x
 
   117   else x
 
   104   else x
 
   118 *}
 
   105 *}
 
   119 
   106 
   120 ML {*
 
   107 ML {*
 
   121 fun fv_body thy dts args fv_frees supp i =
 
   108 fun make_body fv_map args i = 
   122 let
 
   109 let
 
   123   val x = nth args i;
 
   110   val arg = nth args i
 
   124   val dt = nth dts i;
 
   111   val ty = fastype_of arg
 
   125 in
 
   112 in
 
   126   if Datatype_Aux.is_rec_type dt
 
   113   case (AList.lookup (op=) fv_map ty) of
 
   127   then nth fv_frees (Datatype_Aux.body_index dt) $ x
 
   114     NONE => mk_supp arg
 
   128   else (if supp then mk_supp x else setify thy x)
 
   115   | SOME fv => fv $ arg
 
   129 end
 
   116 end  
   130 *}
 
   117 *}
 
   131 
   118 
   132 ML {*
 
   119 ML {*
 
   133 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =
 
   120 fun make_binder lthy fv_bn_map args (bn_option, i) = 
   134 let
 
   121 let
 
   135   val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys)
 
   122   val arg = nth args i
 
   136   fun bound_var (SOME bn, i) = set (bn $ nth args i)
 
   123 in
 
   137     | bound_var (NONE, i) = fv_body thy dts args fv_frees false i
 
   124   case bn_option of
 
   138   val bound_vars = mk_union (map bound_var binds);
 
   125     NONE => (setify lthy arg, @{term "{}::atom set"})
 
   139   fun non_rec_var (SOME bn, i) =
 
   126   | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg)
 
   140       if member (op =) bodys i
 
   127 end  
   141       then noatoms
 
   128 *}
 
   142       else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
 
   129 
   143     | non_rec_var (NONE, _) = noatoms
 
   130 ML {*
 
   144 in
 
   131 fun make_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
 
   145   mk_union ((mk_diff fv_bodys bound_vars) :: (map non_rec_var binds))
 
   132 let
 
   146 end
 
   133   val t1 = map (make_body fv_map args) bodies
 
   147 *}
 
   134   val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders)
 
   148 
   135 in 
   149 ML {*
 
   136   fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
 
   150 fun fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn bm =
 
   137 end
 
   151 case bm of
 
   138 *}
 
   152   BEmy i =>
 
   139 
   153     let
 
   140 ML {*
 
   154       val x = nth args i;
 
   141 fun make_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = 
   155       val dt = nth dts i;
 
   142 let
 
   156     in
 
   143   val arg_names = Datatype_Prop.make_tnames arg_tys
 
   157       case AList.lookup (op=) args_in_bn i of
 
   144   val args = map Free (arg_names ~~ arg_tys)
 
   158         NONE => if Datatype_Aux.is_rec_type dt
 
   145   val fv = the (AList.lookup (op=) fv_map ty)
 
   159                 then nth fv_frees (Datatype_Aux.body_index dt) $ x
 
   146   val lhs = fv $ list_comb (constr, args)
 
   160                 else mk_supp x
 
   147   val rhs_trms = map (make_fv_rhs lthy fv_map fv_bn_map args) bclauses
 
   161       | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x
 
   148   val rhs = fold_union rhs_trms
 
   162       | SOME NONE => noatoms
 
   149 in
 
   163     end
 
   150   HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
 
   164 | BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   151 end
 
   165 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   152 *}
 
   166 | BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   153 
   167 *}
 
   154 ML {*
 
   168 
   155 fun make_bn_body fv_map fv_bn_map bn_args args i = 
   169 ML {*
 
   156 let
 
   170 fun fv_bn thy dt_descr sorts fv_frees bn_fvbn bclausess (fvbn, (_, ith_dtyp, args_in_bns)) =
 
   157   val arg = nth args i
 
   171 let
 
   158   val ty = fastype_of arg
 
   172   fun fv_bn_constr (cname, dts) (args_in_bn, bclauses) =
 
   159 in
 
   173   let
 
   160   case AList.lookup (op=) bn_args i of
 
   174     val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
 
   161     NONE => (case (AList.lookup (op=) fv_map ty) of
 
   175     val names = Datatype_Prop.make_tnames Ts;
 
   162               NONE => mk_supp arg
 
   176     val args = map Free (names ~~ Ts);
 
   163             | SOME fv => fv $ arg)
 
   177     val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
 
   164   | SOME (NONE) => @{term "{}::atom set"}
 
   178     val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn
 
   165   | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
 
   179   in
 
   166 end  
   180     HOLogic.mk_Trueprop (HOLogic.mk_eq
 
   167 *}
 
   181       (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bclauses)))
 
   168 
   182   end;
 
   169 ML {*
 
   183   val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
 
   170 fun make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =
 
   184 in
 
   171   case bclause of
 
   185   map2 fv_bn_constr constrs (args_in_bns ~~ bclausess)
 
   172     BC (_, [], bodies) => fold_union (map (make_bn_body fv_map fv_bn_map bn_args args) bodies)
 
   186 end
 
   173   | BC (_, binders, bodies) => 
   187 *}
 
   174       let
 
   188 
   175         val t1 = map (make_body fv_map args) bodies
 
   189 ML {*
 
   176         val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders)
 
   190 fun fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss =
 
   177       in 
   191 let
 
   178         fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
 
   192   fun mk_fvbn_free (bn, ith, _) =
 
   179       end
 
   193     let
 
   180 *}
 
   194       val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));
 
   181 
   195     in
 
   182 ML {*
 
   196       (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith)))
 
   183 fun make_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, ty, arg_tys)) bclauses =
 
   197     end;
 
   184 let
 
   198 
   185   val arg_names = Datatype_Prop.make_tnames arg_tys
 
   199   val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs);
 
   186   val args = map Free (arg_names ~~ arg_tys)
 
   200   val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees
 
   187   val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm)
 
   201   val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs;
 
   188   val lhs = fv_bn $ list_comb (constr, args)
 
   202   val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bclausessl (fvbn_frees ~~ bn_funs);
 
   189   val rhs_trms = map (make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
 
   203 in
 
   190   val rhs = fold_union rhs_trms
 
   204   (bn_fvbn, fvbn_names, eqs)
 
   191 in
 
   205 end
 
   192   HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
 
   206 *}
 
   193 end
 
   207 
   194 *}
 
   208 ML {*
 
   195 
   209 fun fv_bm thy dts args fv_frees bn_fvbn bm =
 
   196 ML {*
 
   210 case bm of
 
   197 fun make_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 
   211   BEmy i =>
 
   198 let
 
   212     let
 
   199   val nth_constrs_info = nth constrs_info bn_n
 
   213       val x = nth args i;
 
   200   val nth_bclausess = nth bclausesss bn_n
 
   214       val dt = nth dts i;
 
   201 in
 
   215     in
 
   202   map2 (make_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
 
   216       if Datatype_Aux.is_rec_type dt
 
   203 end
 
   217       then nth fv_frees (Datatype_Aux.body_index dt) $ x
 
   204 *}
 
   218       else mk_supp x
 
   205 
   219     end
 
   206 ML {*
 
   220 | BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   207 fun define_raw_fvs dt_descr sorts bn_funs bn_funs2 bclausesss lthy =
 
   221 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
   208 let
 
   222 | BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 
       
   223 *}
 
       
   224 
       
   225 ML {*
 
       
   226 fun fv thy dt_descr sorts fv_frees bn_fvbn bclausess (fv_free, ith_dtyp) =
 
       
   227 let
 
       
   228   fun fv_constr (cname, dts) bclauses =
 
       
   229   let
 
       
   230     val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
 
       
   231     val names = Datatype_Prop.make_tnames Ts;
 
       
   232     val args = map Free (names ~~ Ts);
 
       
   233     val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
 
       
   234     val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn
 
       
   235   in
 
       
   236     HOLogic.mk_Trueprop (HOLogic.mk_eq
 
       
   237       (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bclauses)))
 
       
   238   end;
 
       
   239   val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
 
       
   240 in
 
       
   241   map2 fv_constr constrs bclausess
 
       
   242 end
 
       
   243 *}
 
       
   244 
       
   245 ML {*
 
       
   246 fun define_raw_fvs dt_descr sorts bn_funs bclausesss lthy =
 
       
   247 let
 
       
   248   val thy = ProofContext.theory_of lthy;
 
       
   249 
   209 
   250   val fv_names = prefix_dt_names dt_descr sorts "fv_"
 
   210   val fv_names = prefix_dt_names dt_descr sorts "fv_"
 
   251   val fv_types = map (fn (i, _) => nth_dtyp dt_descr sorts i --> @{typ "atom set"}) dt_descr;
 
   211   val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr;
 
   252   val fv_frees = map Free (fv_names ~~ fv_types);
 
   212   val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;
 
   253 
   213   val fv_frees = map Free (fv_names ~~ fv_tys);
 
   254   (* free variables for the bn-functions *)
 
   214   val fv_map = fv_arg_tys ~~ fv_frees
 
   255   val (bn_fvbn_map, fv_bn_names, fv_bn_eqs) =
 
   215 
   256     fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss;
 
   216   val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs)
 
   257 
   217   val (bns2, bn_tys2) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs2)
 
   258   val _ = tracing ("bn_fvbn_map" ^ commas (map @{make_string} bn_fvbn_map))
 
   218   val bn_args2 = map (fn (_, _, arg) => arg) bn_funs2
 
       
   219   val fv_bn_names2 = map (fn bn => "fv_" ^ (fst (dest_Free bn))) bns2
 
       
   220   val fv_bn_arg_tys2 = map (fn i => nth_dtyp dt_descr sorts i) bn_tys2
 
       
   221   val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2
 
       
   222   val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2)
 
       
   223   val fv_bn_map2 = bns ~~ fv_bn_frees2
 
       
   224   val fv_bn_map3 = bns2 ~~ fv_bn_frees2
 
       
   225  
       
   226   val constrs_info = all_dtyp_constrs_types dt_descr sorts
 
       
   227 
       
   228   val fv_eqs2 = map2 (map2 (make_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss 
       
   229   val fv_bn_eqs2 = map (make_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2
 
   259   
   230   
   260   val fv_bns = map snd bn_fvbn_map;
 
   231   val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2)
 
   261   val fv_nums = 0 upto (length fv_frees - 1)
 
   232   val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2)
 
   262 
   233 
   263   val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn_map) bclausesss (fv_frees ~~ fv_nums);
 
   234   fun pat_completeness_auto lthy =
 
   264 
   235     Pat_Completeness.pat_completeness_tac lthy 1
 
   265   val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
 
   236       THEN auto_tac (clasimpset_of lthy)
 
   266   val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
 
       
   267 
       
   268   fun pat_completeness_auto ctxt =
 
       
   269     Pat_Completeness.pat_completeness_tac ctxt 1
 
       
   270       THEN auto_tac (clasimpset_of ctxt)
 
       
   271 
   237 
   272   fun prove_termination lthy =
 
   238   fun prove_termination lthy =
 
   273     Function.prove_termination NONE
 
   239     Function.prove_termination NONE
 
   274       (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
 
   240       (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
 
   275 
   241 
   288 in
 
   254 in
 
   289   (fv_frees_exp, fv_bns_exp, simps_exp, lthy'')
 
   255   (fv_frees_exp, fv_bns_exp, simps_exp, lthy'')
 
   290 end
 
   256 end
 
   291 *}
 
   257 *}
 
   292 
   258 
   293 (**************************************************)
 
   259 
   294 
   260 
   295 datatype foo =
 
   261 
   296   C1 nat
 
   262 
   297 | C2 foo int
 
   263 end
 
   298 
       
   299 (*
 
       
   300 ML {* 
       
   301 fun mk_body descr sorts fv_ty_map dtyp =
 
       
   302 let
 
       
   303   val nth_dtyp_constr_tys descr sorts
 
       
   304 in
 
       
   305   true
 
       
   306 end
 
       
   307 *}
 
       
   308 *)
 
       
   309 
       
   310 end
nominal2