src/HOL/Tools/datatype_package.ML
changeset 20715 c1f16b427d86
parent 20597 65fe827aa595
child 20820 58693343905f
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Sep 26 13:34:17 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Sep 26 13:34:35 2006 +0200
     1.3 @@ -404,8 +404,8 @@
     1.4        fun case_error s name ts = raise TERM ("Error in case expression" ^
     1.5          getOpt (Option.map (curry op ^ " for datatype ") name, "") ^ ":\n" ^ s, ts);
     1.6        fun dest_case1 (Const ("_case1", _) $ t $ u) = (case strip_comb t of
     1.7 -            (Const (s, _), ts) => (Sign.intern_const thy s, ts)
     1.8 -          | (Free (s, _), ts) => (Sign.intern_const thy s, ts)
     1.9 +            (Const (s, _), ts) => (((perhaps o try o unprefix) Syntax.constN o Sign.intern_const thy) s, ts)
    1.10 +          | (Free (s, _), ts) => (Sign.intern_const thy s, ts) (*FIXME?*)
    1.11            | _ => case_error "Head is not a constructor" NONE [t, u], u)
    1.12          | dest_case1 t = raise TERM ("dest_case1", [t]);
    1.13        fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
    1.14 @@ -817,12 +817,11 @@
    1.15        |> fold_map apply_theorems raw_distinct
    1.16        ||>> fold_map apply_theorems raw_inject
    1.17        ||>> apply_theorems [raw_induction];
    1.18 -    val sign = Theory.sign_of thy1;
    1.19  
    1.20      val ((_, [induction']), _) = Variable.importT [induction] (Variable.thm_context induction);
    1.21  
    1.22      fun err t = error ("Ill-formed predicate in induction rule: " ^
    1.23 -      Sign.string_of_term sign t);
    1.24 +      Sign.string_of_term thy1 t);
    1.25  
    1.26      fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
    1.27            ((tname, map dest_TFree Ts) handle TERM _ => err t)
    1.28 @@ -850,8 +849,12 @@
    1.29      val sorts = add_term_tfrees (concl_of induction', []);
    1.30      val dt_info = get_datatypes thy1;
    1.31  
    1.32 -    val case_names_induct = mk_case_names_induct descr;
    1.33 -    val case_names_exhausts = mk_case_names_exhausts descr (map #1 dtnames);
    1.34 +    val (case_names_induct, case_names_exhausts) = case RuleCases.get induction
    1.35 +     of (("1", _) :: _, _) => (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames))
    1.36 +      | (cases, _) => (RuleCases.case_names (map fst cases),
    1.37 +          replicate (length ((List.filter (fn ((_, (name, _, _))) => member (op =)
    1.38 +            (map #1 dtnames) name) descr)))
    1.39 +            (RuleCases.case_names (map fst cases)));
    1.40      
    1.41  
    1.42      val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);