re-established reasonable inner outline for module
authorhaftmann
Sun Sep 27 20:15:45 2009 +0200 (2009-09-27)
changeset 327170e787c721fa3
parent 32715 becd87e4039b
child 32718 45929374f1bd
re-established reasonable inner outline for module
src/HOL/Tools/Datatype/datatype.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 19:58:24 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 20:15:45 2009 +0200
     1.3 @@ -39,8 +39,9 @@
     1.4  
     1.5  open DatatypeAux;
     1.6  
     1.7 +(** theory data **)
     1.8  
     1.9 -(* theory data *)
    1.10 +(* data management *)
    1.11  
    1.12  structure DatatypesData = TheoryDataFun
    1.13  (
    1.14 @@ -62,13 +63,16 @@
    1.15  );
    1.16  
    1.17  val get_all = #types o DatatypesData.get;
    1.18 -val map_datatypes = DatatypesData.map;
    1.19 -
    1.20 +val get_info = Symtab.lookup o get_all;
    1.21 +fun the_info thy name = (case get_info thy name of
    1.22 +      SOME info => info
    1.23 +    | NONE => error ("Unknown datatype " ^ quote name));
    1.24  
    1.25 -(** theory information about datatypes **)
    1.26 +val info_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
    1.27 +val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
    1.28  
    1.29 -fun put_dt_infos (dt_infos : (string * info) list) =
    1.30 -  map_datatypes (fn {types, constrs, cases} =>
    1.31 +fun register (dt_infos : (string * info) list) =
    1.32 +  DatatypesData.map (fn {types, constrs, cases} =>
    1.33      {types = fold Symtab.update dt_infos types,
    1.34       constrs = fold Symtab.default (*conservative wrt. overloaded constructors*)
    1.35         (maps (fn (_, info as {descr, index, ...}) => map (rpair info o fst)
    1.36 @@ -77,19 +81,7 @@
    1.37         (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)
    1.38         cases});
    1.39  
    1.40 -val get_info = Symtab.lookup o get_all;
    1.41 -
    1.42 -fun the_info thy name = (case get_info thy name of
    1.43 -      SOME info => info
    1.44 -    | NONE => error ("Unknown datatype " ^ quote name));
    1.45 -
    1.46 -val info_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
    1.47 -val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
    1.48 -
    1.49 -fun get_info_descr thy dtco =
    1.50 -  get_info thy dtco
    1.51 -  |> Option.map (fn info as { descr, index, ... } =>
    1.52 -       (info, (((fn SOME (_, dtys, cos) => (dtys, cos)) o AList.lookup (op =) descr) index)));
    1.53 +(* complex queries *)
    1.54  
    1.55  fun the_spec thy dtco =
    1.56    let
    1.57 @@ -143,69 +135,9 @@
    1.58      | NONE => NONE;
    1.59  
    1.60  
    1.61 -(** induct method setup **)
    1.62 -
    1.63 -(* case names *)
    1.64 -
    1.65 -local
    1.66 -
    1.67 -fun dt_recs (DtTFree _) = []
    1.68 -  | dt_recs (DtType (_, dts)) = maps dt_recs dts
    1.69 -  | dt_recs (DtRec i) = [i];
    1.70 -
    1.71 -fun dt_cases (descr: descr) (_, args, constrs) =
    1.72 -  let
    1.73 -    fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
    1.74 -    val bnames = map the_bname (distinct (op =) (maps dt_recs args));
    1.75 -  in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
    1.76 -
    1.77 -
    1.78 -fun induct_cases descr =
    1.79 -  DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
    1.80 -
    1.81 -fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
    1.82 -
    1.83 -in
    1.84 -
    1.85 -fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
    1.86 -
    1.87 -fun mk_case_names_exhausts descr new =
    1.88 -  map (RuleCases.case_names o exhaust_cases descr o #1)
    1.89 -    (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
    1.90 -
    1.91 -end;
    1.92 +(** various auxiliary **)
    1.93  
    1.94 -fun add_rules simps case_thms rec_thms inject distinct
    1.95 -                  weak_case_congs cong_att =
    1.96 -  PureThy.add_thmss [((Binding.name "simps", simps), []),
    1.97 -    ((Binding.empty, flat case_thms @
    1.98 -          flat distinct @ rec_thms), [Simplifier.simp_add]),
    1.99 -    ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
   1.100 -    ((Binding.empty, flat inject), [iff_add]),
   1.101 -    ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
   1.102 -    ((Binding.empty, weak_case_congs), [cong_att])]
   1.103 -  #> snd;
   1.104 -
   1.105 -
   1.106 -(* add_cases_induct *)
   1.107 -
   1.108 -fun add_cases_induct infos inducts thy =
   1.109 -  let
   1.110 -    fun named_rules (name, {index, exhaust, ...}: info) =
   1.111 -      [((Binding.empty, nth inducts index), [Induct.induct_type name]),
   1.112 -       ((Binding.empty, exhaust), [Induct.cases_type name])];
   1.113 -    fun unnamed_rule i =
   1.114 -      ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
   1.115 -  in
   1.116 -    thy |> PureThy.add_thms
   1.117 -      (maps named_rules infos @
   1.118 -        map unnamed_rule (length infos upto length inducts - 1)) |> snd
   1.119 -    |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
   1.120 -  end;
   1.121 -
   1.122 -
   1.123 -
   1.124 -(**** simplification procedure for showing distinctness of constructors ****)
   1.125 +(* simplification procedure for showing distinctness of constructors *)
   1.126  
   1.127  fun stripT (i, Type ("fun", [_, T])) = stripT (i + 1, T)
   1.128    | stripT p = p;
   1.129 @@ -233,17 +165,21 @@
   1.130            etac FalseE 1]))
   1.131        end;
   1.132  
   1.133 +fun get_constr thy dtco =
   1.134 +  get_info thy dtco
   1.135 +  |> Option.map (fn { descr, index, ... } => (#3 o the o AList.lookup (op =) descr) index);
   1.136 +
   1.137  fun distinct_proc thy ss (t as Const ("op =", _) $ t1 $ t2) =
   1.138    (case (stripC (0, t1), stripC (0, t2)) of
   1.139       ((i, Const (cname1, T1)), (j, Const (cname2, T2))) =>
   1.140           (case (stripT (0, T1), stripT (0, T2)) of
   1.141              ((i', Type (tname1, _)), (j', Type (tname2, _))) =>
   1.142                  if tname1 = tname2 andalso not (cname1 = cname2) andalso i = i' andalso j = j' then
   1.143 -                   (case (get_info_descr thy) tname1 of
   1.144 -                      SOME (_, (_, constrs)) => let val cnames = map fst constrs
   1.145 +                   (case get_constr thy tname1 of
   1.146 +                      SOME constrs => let val cnames = map fst constrs
   1.147                          in if cname1 mem cnames andalso cname2 mem cnames then
   1.148                               SOME (distinct_rule thy ss tname1
   1.149 -                               (Logic.mk_equals (t, Const ("False", HOLogic.boolT))))
   1.150 +                               (Logic.mk_equals (t, HOLogic.false_const)))
   1.151                             else NONE
   1.152                          end
   1.153                      | NONE => NONE)
   1.154 @@ -260,29 +196,7 @@
   1.155  val simproc_setup =
   1.156    Simplifier.map_simpset (fn ss => ss addsimprocs [distinct_simproc]);
   1.157  
   1.158 -
   1.159 -(**** translation rules for case ****)
   1.160 -
   1.161 -fun make_case ctxt = DatatypeCase.make_case
   1.162 -  (info_of_constr (ProofContext.theory_of ctxt)) ctxt;
   1.163 -
   1.164 -fun strip_case ctxt = DatatypeCase.strip_case
   1.165 -  (info_of_case (ProofContext.theory_of ctxt));
   1.166 -
   1.167 -fun add_case_tr' case_names thy =
   1.168 -  Sign.add_advanced_trfuns ([], [],
   1.169 -    map (fn case_name =>
   1.170 -      let val case_name' = Sign.const_syntax_name thy case_name
   1.171 -      in (case_name', DatatypeCase.case_tr' info_of_case case_name')
   1.172 -      end) case_names, []) thy;
   1.173 -
   1.174 -val trfun_setup =
   1.175 -  Sign.add_advanced_trfuns ([],
   1.176 -    [("_case_syntax", DatatypeCase.case_tr true info_of_constr)],
   1.177 -    [], []);
   1.178 -
   1.179 -
   1.180 -(* prepare types *)
   1.181 +(* prepare datatype specifications *)
   1.182  
   1.183  fun read_typ thy ((Ts, sorts), str) =
   1.184    let
   1.185 @@ -302,8 +216,7 @@
   1.186         | dups => error ("Inconsistent sort constraints for " ^ commas dups))
   1.187    end;
   1.188  
   1.189 -
   1.190 -(**** make datatype info ****)
   1.191 +(* arrange data entries *)
   1.192  
   1.193  fun make_dt_info alt_names descr sorts inducts reccomb_names rec_thms
   1.194      ((((((((((i, (_, (tname, _, _))), case_name), case_thms),
   1.195 @@ -326,62 +239,113 @@
   1.196      case_cong = case_cong,
   1.197      weak_case_cong = weak_case_cong});
   1.198  
   1.199 +(* case names *)
   1.200 +
   1.201 +local
   1.202 +
   1.203 +fun dt_recs (DtTFree _) = []
   1.204 +  | dt_recs (DtType (_, dts)) = maps dt_recs dts
   1.205 +  | dt_recs (DtRec i) = [i];
   1.206 +
   1.207 +fun dt_cases (descr: descr) (_, args, constrs) =
   1.208 +  let
   1.209 +    fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
   1.210 +    val bnames = map the_bname (distinct (op =) (maps dt_recs args));
   1.211 +  in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
   1.212 +
   1.213 +fun induct_cases descr =
   1.214 +  DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
   1.215 +
   1.216 +fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
   1.217 +
   1.218 +in
   1.219 +
   1.220 +fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
   1.221 +
   1.222 +fun mk_case_names_exhausts descr new =
   1.223 +  map (RuleCases.case_names o exhaust_cases descr o #1)
   1.224 +    (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
   1.225 +
   1.226 +end;
   1.227 +
   1.228 +(* note rules and interpretations *)
   1.229 +
   1.230 +fun add_rules simps case_thms rec_thms inject distinct
   1.231 +                  weak_case_congs cong_att =
   1.232 +  PureThy.add_thmss [((Binding.name "simps", simps), []),
   1.233 +    ((Binding.empty, flat case_thms @
   1.234 +          flat distinct @ rec_thms), [Simplifier.simp_add]),
   1.235 +    ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
   1.236 +    ((Binding.empty, flat inject), [iff_add]),
   1.237 +    ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
   1.238 +    ((Binding.empty, weak_case_congs), [cong_att])]
   1.239 +  #> snd;
   1.240 +
   1.241 +fun add_cases_induct infos inducts thy =
   1.242 +  let
   1.243 +    fun named_rules (name, {index, exhaust, ...}: info) =
   1.244 +      [((Binding.empty, nth inducts index), [Induct.induct_type name]),
   1.245 +       ((Binding.empty, exhaust), [Induct.cases_type name])];
   1.246 +    fun unnamed_rule i =
   1.247 +      ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
   1.248 +  in
   1.249 +    thy |> PureThy.add_thms
   1.250 +      (maps named_rules infos @
   1.251 +        map unnamed_rule (length infos upto length inducts - 1)) |> snd
   1.252 +    |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
   1.253 +  end;
   1.254 +
   1.255  structure DatatypeInterpretation = InterpretationFun
   1.256    (type T = config * string list val eq: T * T -> bool = eq_snd op =);
   1.257  fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
   1.258  
   1.259 +(* translation rules for case *)
   1.260  
   1.261 -(******************* definitional introduction of datatypes *******************)
   1.262 +fun make_case ctxt = DatatypeCase.make_case
   1.263 +  (info_of_constr (ProofContext.theory_of ctxt)) ctxt;
   1.264 +
   1.265 +fun strip_case ctxt = DatatypeCase.strip_case
   1.266 +  (info_of_case (ProofContext.theory_of ctxt));
   1.267  
   1.268 -fun add_datatype_def (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
   1.269 -    case_names_induct case_names_exhausts thy =
   1.270 -  let
   1.271 -    val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
   1.272 +fun add_case_tr' case_names thy =
   1.273 +  Sign.add_advanced_trfuns ([], [],
   1.274 +    map (fn case_name =>
   1.275 +      let val case_name' = Sign.const_syntax_name thy case_name
   1.276 +      in (case_name', DatatypeCase.case_tr' info_of_case case_name')
   1.277 +      end) case_names, []) thy;
   1.278  
   1.279 -    val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
   1.280 -      DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
   1.281 -        types_syntax constr_syntax case_names_induct;
   1.282 -    val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
   1.283 +val trfun_setup =
   1.284 +  Sign.add_advanced_trfuns ([],
   1.285 +    [("_case_syntax", DatatypeCase.case_tr true info_of_constr)],
   1.286 +    [], []);
   1.287 +
   1.288 +(* document antiquotation *)
   1.289  
   1.290 -    val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
   1.291 -      sorts induct case_names_exhausts thy2;
   1.292 -    val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
   1.293 -      config new_type_names descr sorts dt_info inject dist_rewrites
   1.294 -      (Simplifier.theory_context thy3 dist_ss) induct thy3;
   1.295 -    val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
   1.296 -      config new_type_names descr sorts reccomb_names rec_thms thy4;
   1.297 -    val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms config new_type_names
   1.298 -      descr sorts inject dist_rewrites casedist_thms case_thms thy6;
   1.299 -    val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys config new_type_names
   1.300 -      descr sorts casedist_thms thy7;
   1.301 -    val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
   1.302 -      descr sorts nchotomys case_thms thy8;
   1.303 -    val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
   1.304 -      descr sorts thy9;
   1.305 -
   1.306 -    val dt_infos = map
   1.307 -      (make_dt_info (SOME new_type_names) (flat descr) sorts (inducts, induct) reccomb_names rec_thms)
   1.308 -      ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_thms ~~
   1.309 -        casedist_thms ~~ simproc_dists ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   1.310 -
   1.311 -    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
   1.312 -    val dt_names = map fst dt_infos;
   1.313 -
   1.314 -    val thy12 =
   1.315 -      thy10
   1.316 -      |> add_case_tr' case_names
   1.317 -      |> Sign.add_path (space_implode "_" new_type_names)
   1.318 -      |> add_rules simps case_thms rec_thms inject distinct
   1.319 -          weak_case_congs (Simplifier.attrib (op addcongs))
   1.320 -      |> put_dt_infos dt_infos
   1.321 -      |> add_cases_induct dt_infos inducts
   1.322 -      |> Sign.parent_path
   1.323 -      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
   1.324 -      |> DatatypeInterpretation.data (config, map fst dt_infos);
   1.325 -  in (dt_names, thy12) end;
   1.326 +val _ = ThyOutput.antiquotation "datatype" Args.tyname
   1.327 +  (fn {source = src, context = ctxt, ...} => fn dtco =>
   1.328 +    let
   1.329 +      val thy = ProofContext.theory_of ctxt;
   1.330 +      val (vs, cos) = the_spec thy dtco;
   1.331 +      val ty = Type (dtco, map TFree vs);
   1.332 +      fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
   1.333 +            Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]
   1.334 +        | pretty_typ_bracket ty =
   1.335 +            Syntax.pretty_typ ctxt ty;
   1.336 +      fun pretty_constr (co, tys) =
   1.337 +        (Pretty.block o Pretty.breaks)
   1.338 +          (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
   1.339 +            map pretty_typ_bracket tys);
   1.340 +      val pretty_datatype =
   1.341 +        Pretty.block
   1.342 +          (Pretty.command "datatype" :: Pretty.brk 1 ::
   1.343 +           Syntax.pretty_typ ctxt ty ::
   1.344 +           Pretty.str " =" :: Pretty.brk 1 ::
   1.345 +           flat (separate [Pretty.brk 1, Pretty.str "| "]
   1.346 +             (map (single o pretty_constr) cos)));
   1.347 +    in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
   1.348  
   1.349  
   1.350 -(*********************** declare existing type as datatype *********************)
   1.351 +(** declare existing type as datatype **)
   1.352  
   1.353  fun prove_rep_datatype (config : config) alt_names new_type_names descr sorts induct inject half_distinct thy =
   1.354    let
   1.355 @@ -441,7 +405,7 @@
   1.356        |> add_case_tr' case_names
   1.357        |> add_rules simps case_thms rec_thms inject distinct
   1.358             weak_case_congs (Simplifier.attrib (op addcongs))
   1.359 -      |> put_dt_infos dt_infos
   1.360 +      |> register dt_infos
   1.361        |> add_cases_induct dt_infos inducts
   1.362        |> Sign.parent_path
   1.363        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
   1.364 @@ -518,8 +482,54 @@
   1.365  val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
   1.366  
   1.367  
   1.368 +(** definitional introduction of datatypes **)
   1.369  
   1.370 -(******************************** add datatype ********************************)
   1.371 +fun add_datatype_def (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
   1.372 +    case_names_induct case_names_exhausts thy =
   1.373 +  let
   1.374 +    val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
   1.375 +
   1.376 +    val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
   1.377 +      DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
   1.378 +        types_syntax constr_syntax case_names_induct;
   1.379 +    val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
   1.380 +
   1.381 +    val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
   1.382 +      sorts induct case_names_exhausts thy2;
   1.383 +    val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
   1.384 +      config new_type_names descr sorts dt_info inject dist_rewrites
   1.385 +      (Simplifier.theory_context thy3 dist_ss) induct thy3;
   1.386 +    val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
   1.387 +      config new_type_names descr sorts reccomb_names rec_thms thy4;
   1.388 +    val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms config new_type_names
   1.389 +      descr sorts inject dist_rewrites casedist_thms case_thms thy6;
   1.390 +    val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys config new_type_names
   1.391 +      descr sorts casedist_thms thy7;
   1.392 +    val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
   1.393 +      descr sorts nchotomys case_thms thy8;
   1.394 +    val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
   1.395 +      descr sorts thy9;
   1.396 +
   1.397 +    val dt_infos = map
   1.398 +      (make_dt_info (SOME new_type_names) (flat descr) sorts (inducts, induct) reccomb_names rec_thms)
   1.399 +      ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_thms ~~
   1.400 +        casedist_thms ~~ simproc_dists ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   1.401 +
   1.402 +    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
   1.403 +    val dt_names = map fst dt_infos;
   1.404 +
   1.405 +    val thy12 =
   1.406 +      thy10
   1.407 +      |> add_case_tr' case_names
   1.408 +      |> Sign.add_path (space_implode "_" new_type_names)
   1.409 +      |> add_rules simps case_thms rec_thms inject distinct
   1.410 +          weak_case_congs (Simplifier.attrib (op addcongs))
   1.411 +      |> register dt_infos
   1.412 +      |> add_cases_induct dt_infos inducts
   1.413 +      |> Sign.parent_path
   1.414 +      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
   1.415 +      |> DatatypeInterpretation.data (config, map fst dt_infos);
   1.416 +  in (dt_names, thy12) end;
   1.417  
   1.418  fun gen_add_datatype prep_typ (config : config) new_type_names dts thy =
   1.419    let
   1.420 @@ -596,7 +606,6 @@
   1.421  val datatype_cmd = snd ooo gen_add_datatype read_typ default_config;
   1.422  
   1.423  
   1.424 -
   1.425  (** package setup **)
   1.426  
   1.427  (* setup theory *)
   1.428 @@ -607,7 +616,6 @@
   1.429    trfun_setup #>
   1.430    DatatypeInterpretation.init;
   1.431  
   1.432 -
   1.433  (* outer syntax *)
   1.434  
   1.435  local
   1.436 @@ -642,31 +650,5 @@
   1.437  
   1.438  end;
   1.439  
   1.440 -
   1.441 -(* document antiquotation *)
   1.442 -
   1.443 -val _ = ThyOutput.antiquotation "datatype" Args.tyname
   1.444 -  (fn {source = src, context = ctxt, ...} => fn dtco =>
   1.445 -    let
   1.446 -      val thy = ProofContext.theory_of ctxt;
   1.447 -      val (vs, cos) = the_spec thy dtco;
   1.448 -      val ty = Type (dtco, map TFree vs);
   1.449 -      fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
   1.450 -            Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]
   1.451 -        | pretty_typ_bracket ty =
   1.452 -            Syntax.pretty_typ ctxt ty;
   1.453 -      fun pretty_constr (co, tys) =
   1.454 -        (Pretty.block o Pretty.breaks)
   1.455 -          (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
   1.456 -            map pretty_typ_bracket tys);
   1.457 -      val pretty_datatype =
   1.458 -        Pretty.block
   1.459 -          (Pretty.command "datatype" :: Pretty.brk 1 ::
   1.460 -           Syntax.pretty_typ ctxt ty ::
   1.461 -           Pretty.str " =" :: Pretty.brk 1 ::
   1.462 -           flat (separate [Pretty.brk 1, Pretty.str "| "]
   1.463 -             (map (single o pretty_constr) cos)));
   1.464 -    in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
   1.465 -
   1.466  end;
   1.467