src/HOL/Tools/datatype_package.ML
changeset 18319 c52b139ebde0
parent 18314 4595eb4627fa
child 18377 0e1d025d57b3
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Dec 01 18:37:39 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Dec 01 18:39:08 2005 +0100
     1.3 @@ -404,12 +404,11 @@
     1.4      in case find_first (fn (_, {descr, index, ...}) =>
     1.5        exists (equal cname o fst) (#3 (snd (List.nth (descr, index))))) tab of
     1.6          NONE => case_error ("Not a datatype constructor: " ^ cname) NONE [u]
     1.7 -      | SOME (tname, {descr, case_name, index, ...}) =>
     1.8 +      | SOME (tname, {descr, sorts, case_name, index, ...}) =>
     1.9          let
    1.10            val _ = if exists (equal "dummy_pattern" o fst o fst) cases' then
    1.11              case_error "Illegal occurrence of '_' dummy pattern" (SOME tname) [u] else ();
    1.12            val (_, (_, dts, constrs)) = List.nth (descr, index);
    1.13 -          val sorts = map (rpair [] o dest_DtTFree) dts;
    1.14            fun find_case (cases, (s, dt)) =
    1.15              (case find_first (equal s o fst o fst) cases' of
    1.16                 NONE => (case default of
    1.17 @@ -509,12 +508,13 @@
    1.18  
    1.19  (**** make datatype info ****)
    1.20  
    1.21 -fun make_dt_info descr induct reccomb_names rec_thms
    1.22 +fun make_dt_info descr sorts induct reccomb_names rec_thms
    1.23      (((((((((i, (_, (tname, _, _))), case_name), case_thms),
    1.24        exhaustion_thm), distinct_thm), inject), nchotomy), case_cong), weak_case_cong) =
    1.25    (tname,
    1.26     {index = i,
    1.27      descr = descr,
    1.28 +    sorts = sorts,
    1.29      rec_names = reccomb_names,
    1.30      rec_rewrites = rec_thms,
    1.31      case_name = case_name,
    1.32 @@ -670,7 +670,7 @@
    1.33      val (thy11, weak_case_congs) = add_and_get_axioms "weak_case_cong" new_type_names
    1.34        (DatatypeProp.make_weak_case_congs new_type_names descr sorts thy10) thy10;
    1.35  
    1.36 -    val dt_infos = map (make_dt_info descr' induct reccomb_names' rec_thms)
    1.37 +    val dt_infos = map (make_dt_info descr' sorts induct reccomb_names' rec_thms)
    1.38        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
    1.39          exhaustion ~~ replicate (length (hd descr)) QuickAndDirty ~~ inject ~~
    1.40            nchotomys ~~ case_congs ~~ weak_case_congs);
    1.41 @@ -729,7 +729,7 @@
    1.42      val (size_thms, thy11) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
    1.43        descr sorts reccomb_names rec_thms thy10;
    1.44  
    1.45 -    val dt_infos = map (make_dt_info (List.concat descr) induct reccomb_names rec_thms)
    1.46 +    val dt_infos = map (make_dt_info (List.concat descr) sorts induct reccomb_names rec_thms)
    1.47        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
    1.48          casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    1.49  
    1.50 @@ -837,7 +837,7 @@
    1.51        Theory.add_path (space_implode "_" new_type_names) |>
    1.52        PureThy.add_thms [(("induct", induction), [case_names_induct])] |> Library.swap;
    1.53  
    1.54 -    val dt_infos = map (make_dt_info descr induction' reccomb_names rec_thms)
    1.55 +    val dt_infos = map (make_dt_info descr sorts induction' reccomb_names rec_thms)
    1.56        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
    1.57          map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    1.58