src/HOL/Tools/inductive_package.ML
changeset 10735 dfaf75f0076f
parent 10729 1b3350c4ee92
child 10743 8ea821d1e3a4
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Dec 23 22:51:01 2000 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Dec 23 22:51:34 2000 +0100
     1.3 @@ -1,7 +1,8 @@
     1.4  (*  Title:      HOL/Tools/inductive_package.ML
     1.5      ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -                Stefan Berghofer,   TU Muenchen
     1.8 +    Author:     Stefan Berghofer, TU Muenchen
     1.9 +    Author:     Markus Wenzel, TU Muenchen
    1.10      Copyright   1994  University of Cambridge
    1.11                  1998  TU Muenchen
    1.12  
    1.13 @@ -39,6 +40,10 @@
    1.14    val mono_add_global: theory attribute
    1.15    val mono_del_global: theory attribute
    1.16    val get_monos: theory -> thm list
    1.17 +  val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
    1.18 +    -> theory -> theory
    1.19 +  val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
    1.20 +    -> theory -> theory
    1.21    val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    1.22      theory attribute list -> ((bstring * term) * theory attribute list) list ->
    1.23        thm list -> thm list -> theory -> theory *
    1.24 @@ -49,10 +54,6 @@
    1.25        (xstring * Args.src list) list -> theory -> theory *
    1.26        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.27         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    1.28 -  val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
    1.29 -    -> theory -> theory
    1.30 -  val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
    1.31 -    -> theory -> theory
    1.32    val setup: (theory -> theory) list
    1.33  end;
    1.34  
    1.35 @@ -62,7 +63,13 @@
    1.36  
    1.37  (** theory context references **)
    1.38  
    1.39 -val mk_inductive_conj = HOLogic.mk_binop "Inductive.conj";
    1.40 +val mono_name = "Ord.mono";
    1.41 +val gfp_name = "Gfp.gfp";
    1.42 +val lfp_name = "Lfp.lfp";
    1.43 +val vimage_name = "Inverse_Image.vimage";
    1.44 +val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
    1.45 +
    1.46 +val inductive_conj_name = "Inductive.conj";
    1.47  val inductive_conj_def = thm "conj_def";
    1.48  val inductive_conj = thms "inductive_conj";
    1.49  val inductive_atomize = thms "inductive_atomize";
    1.50 @@ -71,7 +78,7 @@
    1.51  
    1.52  
    1.53  
    1.54 -(*** theory data ***)
    1.55 +(** theory data **)
    1.56  
    1.57  (* data kind 'HOL/inductive' *)
    1.58  
    1.59 @@ -150,20 +157,18 @@
    1.60  
    1.61  
    1.62  
    1.63 -(** utilities **)
    1.64 -
    1.65 -(* messages *)
    1.66 +(** misc utilities **)
    1.67  
    1.68  val quiet_mode = ref false;
    1.69 -fun message s = if !quiet_mode then () else writeln s;
    1.70 +fun message s = if ! quiet_mode then () else writeln s;
    1.71 +fun clean_message s = if ! quick_and_dirty then () else message s;
    1.72  
    1.73  fun coind_prefix true = "co"
    1.74    | coind_prefix false = "";
    1.75  
    1.76  
    1.77 -(* the following code ensures that each recursive set *)
    1.78 -(* always has the same type in all introduction rules *)
    1.79 -
    1.80 +(*the following code ensures that each recursive set always has the
    1.81 +  same type in all introduction rules*)
    1.82  fun unify_consts sign cs intr_ts =
    1.83    (let
    1.84      val {tsig, ...} = Sign.rep_sg sign;
    1.85 @@ -192,15 +197,7 @@
    1.86      (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
    1.87  
    1.88  
    1.89 -(* misc *)
    1.90 -
    1.91 -val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD);
    1.92 -
    1.93 -val vimage_name = Sign.intern_const (Theory.sign_of Inverse_Image.thy) "vimage";
    1.94 -val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
    1.95 -
    1.96 -(* make injections needed in mutually recursive definitions *)
    1.97 -
    1.98 +(*make injections used in mutually recursive definitions*)
    1.99  fun mk_inj cs sumT c x =
   1.100    let
   1.101      fun mk_inj' T n i =
   1.102 @@ -216,8 +213,7 @@
   1.103    in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
   1.104    end;
   1.105  
   1.106 -(* make "vimage" terms for selecting out components of mutually rec.def. *)
   1.107 -
   1.108 +(*make "vimage" terms for selecting out components of mutually rec.def*)
   1.109  fun mk_vimage cs sumT t c = if length cs < 2 then t else
   1.110    let
   1.111      val cT = HOLogic.dest_setT (fastype_of c);
   1.112 @@ -274,20 +270,13 @@
   1.113    full_simplify inductive_rulify2 o full_simplify inductive_rulify1 o
   1.114    full_simplify inductive_conj;
   1.115  
   1.116 -fun rulified x = Drule.rule_attribute (K rulify) x;
   1.117 -
   1.118  end;
   1.119  
   1.120  
   1.121 -fun try' f msg sign t = (case (try f t) of
   1.122 -      Some x => x
   1.123 -    | None => error (msg ^ Sign.string_of_term sign t));
   1.124 -
   1.125  
   1.126 +(** properties of (co)inductive sets **)
   1.127  
   1.128 -(*** properties of (co)inductive sets ***)
   1.129 -
   1.130 -(** elimination rules **)
   1.131 +(* elimination rules *)
   1.132  
   1.133  fun mk_elims cs cTs params intr_ts intr_names =
   1.134    let
   1.135 @@ -319,8 +308,7 @@
   1.136    end;
   1.137  
   1.138  
   1.139 -
   1.140 -(** premises and conclusions of induction rules **)
   1.141 +(* premises and conclusions of induction rules *)
   1.142  
   1.143  fun mk_indrule cs cTs params intr_ts =
   1.144    let
   1.145 @@ -343,7 +331,7 @@
   1.146          fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
   1.147                (case pred_of u of
   1.148                    None => (m $ fst (subst t) $ fst (subst u), None)
   1.149 -                | Some P => (mk_inductive_conj (s, P $ t), Some (s, P $ t)))
   1.150 +                | Some P => (HOLogic.mk_binop inductive_conj_name (s, P $ t), Some (s, P $ t)))
   1.151            | subst s =
   1.152                (case pred_of s of
   1.153                    Some P => (HOLogic.mk_binop "op Int"
   1.154 @@ -388,8 +376,7 @@
   1.155    end;
   1.156  
   1.157  
   1.158 -
   1.159 -(** prepare cases and induct rules **)
   1.160 +(* prepare cases and induct rules *)
   1.161  
   1.162  (*
   1.163    transform mutual rule:
   1.164 @@ -424,27 +411,23 @@
   1.165  
   1.166  
   1.167  
   1.168 -(*** proofs for (co)inductive sets ***)
   1.169 +(** proofs for (co)inductive sets **)
   1.170  
   1.171 -(** prove monotonicity **)
   1.172 +(* prove monotonicity -- NOT subject to quick_and_dirty! *)
   1.173  
   1.174  fun prove_mono setT fp_fun monos thy =
   1.175 -  let
   1.176 -    val _ = message "  Proving monotonicity ...";
   1.177 -
   1.178 -    val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
   1.179 + (message "  Proving monotonicity ...";
   1.180 +  Goals.prove_goalw_cterm []      (*NO SkipProof.prove_goalw_cterm here!*)
   1.181 +    (Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
   1.182        (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
   1.183 -        (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)])
   1.184 -
   1.185 -  in mono end;
   1.186 +    (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)]));
   1.187  
   1.188  
   1.189 -
   1.190 -(** prove introduction rules **)
   1.191 +(* prove introduction rules *)
   1.192  
   1.193  fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
   1.194    let
   1.195 -    val _ = message "  Proving the introduction rules ...";
   1.196 +    val _ = clean_message "  Proving the introduction rules ...";
   1.197  
   1.198      val unfold = standard (mono RS (fp_def RS
   1.199        (if coind then def_gfp_unfold else def_lfp_unfold)));
   1.200 @@ -453,8 +436,8 @@
   1.201        | select_disj _ 1 = [rtac disjI1]
   1.202        | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
   1.203  
   1.204 -    val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
   1.205 -      (cterm_of (Theory.sign_of thy) intr) (fn prems =>
   1.206 +    val intrs = map (fn (i, intr) => SkipProof.prove_goalw_cterm thy rec_sets_defs
   1.207 +      (Thm.cterm_of (Theory.sign_of thy) intr) (fn prems =>
   1.208         [(*insert prems and underlying sets*)
   1.209         cut_facts_tac prems 1,
   1.210         stac unfold 1,
   1.211 @@ -463,7 +446,7 @@
   1.212         EVERY1 (select_disj (length intr_ts) i),
   1.213         (*Not ares_tac, since refl must be tried before any equality assumptions;
   1.214           backtracking may occur if the premises have extra variables!*)
   1.215 -       DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
   1.216 +       DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
   1.217         (*Now solve the equations like Inl 0 = Inl ?b2*)
   1.218         rewrite_goals_tac con_defs,
   1.219         REPEAT (rtac refl 1)])
   1.220 @@ -472,41 +455,37 @@
   1.221    in (intrs, unfold) end;
   1.222  
   1.223  
   1.224 -
   1.225 -(** prove elimination rules **)
   1.226 +(* prove elimination rules *)
   1.227  
   1.228  fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy =
   1.229    let
   1.230 -    val _ = message "  Proving the elimination rules ...";
   1.231 +    val _ = clean_message "  Proving the elimination rules ...";
   1.232  
   1.233      val rules1 = [CollectE, disjE, make_elim vimageD, exE];
   1.234 -    val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @
   1.235 -      map make_elim [Inl_inject, Inr_inject];
   1.236 +    val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
   1.237    in
   1.238 -    map (fn (t, cases) => prove_goalw_cterm rec_sets_defs
   1.239 -      (cterm_of (Theory.sign_of thy) t) (fn prems =>
   1.240 +    map (fn (t, cases) => SkipProof.prove_goalw_cterm thy rec_sets_defs
   1.241 +      (Thm.cterm_of (Theory.sign_of thy) t) (fn prems =>
   1.242          [cut_facts_tac [hd prems] 1,
   1.243           dtac (unfold RS subst) 1,
   1.244           REPEAT (FIRSTGOAL (eresolve_tac rules1)),
   1.245           REPEAT (FIRSTGOAL (eresolve_tac rules2)),
   1.246 -         EVERY (map (fn prem =>
   1.247 -           DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
   1.248 +         EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
   1.249        |> rulify
   1.250        |> RuleCases.name cases)
   1.251        (mk_elims cs cTs params intr_ts intr_names)
   1.252    end;
   1.253  
   1.254  
   1.255 -(** derivation of simplified elimination rules **)
   1.256 +(* derivation of simplified elimination rules *)
   1.257  
   1.258  (*Applies freeness of the given constructors, which *must* be unfolded by
   1.259    the given defs.  Cannot simply use the local con_defs because con_defs=[]
   1.260 -  for inference systems.
   1.261 - *)
   1.262 +  for inference systems. (??) *)
   1.263  
   1.264  (*cprop should have the form t:Si where Si is an inductive set*)
   1.265  
   1.266 -val mk_cases_err = "mk_cases: proposition not of form 't : S_i'";
   1.267 +val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
   1.268  
   1.269  fun mk_cases_i elims ss cprop =
   1.270    let
   1.271 @@ -561,13 +540,12 @@
   1.272  val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
   1.273  
   1.274  
   1.275 -
   1.276 -(** prove induction rule **)
   1.277 +(* prove induction rule *)
   1.278  
   1.279  fun prove_indrule cs cTs sumT rec_const params intr_ts mono
   1.280      fp_def rec_sets_defs thy =
   1.281    let
   1.282 -    val _ = message "  Proving the induction rule ...";
   1.283 +    val _ = clean_message "  Proving the induction rule ...";
   1.284  
   1.285      val sign = Theory.sign_of thy;
   1.286  
   1.287 @@ -597,15 +575,14 @@
   1.288      (* simplification rules for vimage and Collect *)
   1.289  
   1.290      val vimage_simps = if length cs < 2 then [] else
   1.291 -      map (fn c => prove_goalw_cterm [] (cterm_of sign
   1.292 +      map (fn c => SkipProof.prove_goalw_cterm thy [] (Thm.cterm_of sign
   1.293          (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.294            (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   1.295             HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   1.296               nth_elem (find_index_eq c cs, preds)))))
   1.297 -        (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites,
   1.298 -          rtac refl 1])) cs;
   1.299 +        (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
   1.300  
   1.301 -    val induct = prove_goalw_cterm [inductive_conj_def] (cterm_of sign
   1.302 +    val induct = SkipProof.prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
   1.303        (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   1.304          [rtac (impI RS allI) 1,
   1.305           DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
   1.306 @@ -620,7 +597,7 @@
   1.307           EVERY (map (fn prem =>
   1.308             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
   1.309  
   1.310 -    val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
   1.311 +    val lemma = SkipProof.prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
   1.312        (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
   1.313          [cut_facts_tac prems 1,
   1.314           REPEAT (EVERY
   1.315 @@ -633,9 +610,7 @@
   1.316  
   1.317  
   1.318  
   1.319 -(*** specification of (co)inductive sets ****)
   1.320 -
   1.321 -(** definitional introduction of (co)inductive sets **)
   1.322 +(** specification of (co)inductive sets **)
   1.323  
   1.324  fun cond_declare_consts declare_consts cs paramTs cnames =
   1.325    if declare_consts then
   1.326 @@ -648,8 +623,7 @@
   1.327      val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
   1.328      val setT = HOLogic.mk_setT sumT;
   1.329  
   1.330 -    val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
   1.331 -      else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";
   1.332 +    val fp_name = if coind then gfp_name else lfp_name;
   1.333  
   1.334      val used = foldr add_term_names (intr_ts, []);
   1.335      val [sname, xname] = variantlist (["S", "x"], used);
   1.336 @@ -688,7 +662,7 @@
   1.337        (Const (full_rec_name, paramTs ---> setT), params);
   1.338  
   1.339      val fp_def_term = Logic.mk_equals (rec_const,
   1.340 -      Const (fp_name, (setT --> setT) --> setT) $ fp_fun)
   1.341 +      Const (fp_name, (setT --> setT) --> setT) $ fp_fun);
   1.342  
   1.343      val def_terms = fp_def_term :: (if length cs < 2 then [] else
   1.344        map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
   1.345 @@ -703,15 +677,14 @@
   1.346  
   1.347      val mono = prove_mono setT fp_fun monos thy'
   1.348  
   1.349 -  in
   1.350 -    (thy', mono, fp_def, rec_sets_defs, rec_const, sumT)
   1.351 -  end;
   1.352 +  in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
   1.353  
   1.354  fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   1.355      atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
   1.356    let
   1.357 -    val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
   1.358 -      commas_quote cnames) else ();
   1.359 +    val _ =
   1.360 +      if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
   1.361 +        commas_quote cnames) else ();
   1.362  
   1.363      val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   1.364  
   1.365 @@ -735,17 +708,14 @@
   1.366  
   1.367      val (thy2, intrs') =
   1.368        thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
   1.369 -    val (thy3, [intrs'']) =
   1.370 -      thy2      
   1.371 -      |> PureThy.add_thmss [(("intros", intrs'), atts)]
   1.372 -      |>> (if no_elim then I else #1 o PureThy.add_thmss [(("elims", elims), [])])
   1.373 -      |>> (if no_ind then I else #1 o PureThy.add_thms
   1.374 -        [((coind_prefix coind ^ "induct", rulify induct), [RuleCases.case_names induct_cases])])
   1.375 +    val (thy3, ([intrs'', elims'], [induct'])) =
   1.376 +      thy2
   1.377 +      |> PureThy.add_thmss [(("intros", intrs'), atts), (("elims", elims), [])]
   1.378 +      |>>> PureThy.add_thms
   1.379 +        [((coind_prefix coind ^ "induct", rulify induct), [RuleCases.case_names induct_cases])]
   1.380        |>> Theory.parent_path;
   1.381 -    val elims' = if no_elim then elims else PureThy.get_thms thy3 "elims";  (* FIXME improve *)
   1.382 -    val induct' = if no_ind then induct else PureThy.get_thm thy3 (coind_prefix coind ^ "induct");  (* FIXME improve *)
   1.383    in (thy3,
   1.384 -    {defs = fp_def::rec_sets_defs,
   1.385 +    {defs = fp_def :: rec_sets_defs,
   1.386       mono = mono,
   1.387       unfold = unfold,
   1.388       intrs = intrs'',
   1.389 @@ -756,59 +726,12 @@
   1.390    end;
   1.391  
   1.392  
   1.393 -
   1.394 -(** axiomatic introduction of (co)inductive sets **)
   1.395 -
   1.396 -fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
   1.397 -    atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
   1.398 -  let
   1.399 -    val _ = message (coind_prefix coind ^ "inductive set(s) " ^ commas_quote cnames);
   1.400 -
   1.401 -    val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   1.402 -    val (thy1, _, fp_def, rec_sets_defs, _, _) =
   1.403 -      mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   1.404 -        params paramTs cTs cnames;
   1.405 -    val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names);
   1.406 -    val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   1.407 -    val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
   1.408 -
   1.409 -    val (thy2, [intrs, raw_elims]) =
   1.410 -      thy1
   1.411 -      |> PureThy.add_axiomss_i
   1.412 -        [(("raw_intros", intr_ts), [rulified]),
   1.413 -          (("raw_elims", elim_ts), [rulified])]
   1.414 -      |>> (if coind then I else
   1.415 -            #1 o PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
   1.416 +(* external interfaces *)
   1.417  
   1.418 -    val elims = map2 (fn (th, cases) => RuleCases.name cases th) (raw_elims, elim_cases);
   1.419 -    val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy2 "raw_induct";
   1.420 -    val induct = if coind orelse length cs > 1 then raw_induct
   1.421 -      else standard (raw_induct RSN (2, rev_mp));
   1.422 -
   1.423 -    val (thy3, intrs') =
   1.424 -      thy2 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
   1.425 -    val (thy4, [intrs'', elims']) =
   1.426 -      thy3
   1.427 -      |> PureThy.add_thmss [(("intros", intrs'), atts), (("elims", elims), [])]
   1.428 -      |>> (if coind then I
   1.429 -          else #1 o PureThy.add_thms [(("induct", rulify induct),
   1.430 -            [RuleCases.case_names induct_cases])])
   1.431 -      |>> Theory.parent_path;
   1.432 -    val induct' = if coind then raw_induct else PureThy.get_thm thy4 "induct";
   1.433 -  in (thy4,
   1.434 -    {defs = fp_def :: rec_sets_defs,
   1.435 -     mono = Drule.asm_rl,
   1.436 -     unfold = Drule.asm_rl,
   1.437 -     intrs = intrs'',
   1.438 -     elims = elims',
   1.439 -     mk_cases = mk_cases elims',
   1.440 -     raw_induct = rulify raw_induct,
   1.441 -     induct = induct'})
   1.442 -  end;
   1.443 -
   1.444 -
   1.445 -
   1.446 -(** introduction of (co)inductive sets **)
   1.447 +fun try_term f msg sign t =
   1.448 +  (case Library.try f t of
   1.449 +    Some x => x
   1.450 +  | None => error (msg ^ Sign.string_of_term sign t));
   1.451  
   1.452  fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
   1.453      atts pre_intros monos con_defs thy =
   1.454 @@ -818,13 +741,13 @@
   1.455  
   1.456      (*parameters should agree for all mutually recursive components*)
   1.457      val (_, params) = strip_comb (hd cs);
   1.458 -    val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\
   1.459 +    val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\
   1.460        \ component is not a free variable: " sign) params;
   1.461  
   1.462 -    val cTs = map (try' (HOLogic.dest_setT o fastype_of)
   1.463 +    val cTs = map (try_term (HOLogic.dest_setT o fastype_of)
   1.464        "Recursive component not of type set: " sign) cs;
   1.465  
   1.466 -    val full_cnames = map (try' (fst o dest_Const o head_of)
   1.467 +    val full_cnames = map (try_term (fst o dest_Const o head_of)
   1.468        "Recursive set not previously declared as constant: " sign) cs;
   1.469      val cnames = map Sign.base_name full_cnames;
   1.470  
   1.471 @@ -834,18 +757,13 @@
   1.472      val induct_cases = map (#1 o #1) intros;
   1.473  
   1.474      val (thy1, result as {elims, induct, ...}) =
   1.475 -      (if ! quick_and_dirty andalso not coind (* FIXME *) then add_ind_axm else add_ind_def)
   1.476 -        verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
   1.477 +      add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
   1.478          con_defs thy params paramTs cTs cnames induct_cases;
   1.479      val thy2 = thy1
   1.480        |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
   1.481        |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct induct_cases;
   1.482    in (thy2, result) end;
   1.483  
   1.484 -
   1.485 -
   1.486 -(** external interface **)
   1.487 -
   1.488  fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
   1.489    let
   1.490      val sign = Theory.sign_of thy;
   1.491 @@ -915,5 +833,4 @@
   1.492  
   1.493  end;
   1.494  
   1.495 -
   1.496  end;