src/HOL/Tools/inductive_package.ML
changeset 6394 3d9fd50fcc43
parent 6141 a6922171b396
child 6424 ceab9e663e08
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Mar 17 16:53:32 1999 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Mar 17 16:53:46 1999 +0100
     1.3 @@ -63,8 +63,8 @@
     1.4  (*For simplifying the elimination rule*)
     1.5  val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
     1.6  
     1.7 -val vimage_name = Sign.intern_const (sign_of Vimage.thy) "op -``";
     1.8 -val mono_name = Sign.intern_const (sign_of Ord.thy) "mono";
     1.9 +val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``";
    1.10 +val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
    1.11  
    1.12  (* make injections needed in mutually recursive definitions *)
    1.13  
    1.14 @@ -225,7 +225,7 @@
    1.15    let
    1.16      val _ = message "  Proving monotonicity...";
    1.17  
    1.18 -    val mono = prove_goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop
    1.19 +    val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
    1.20        (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
    1.21          (fn _ => [rtac monoI 1, REPEAT (ares_tac (basic_monos @ monos) 1)])
    1.22  
    1.23 @@ -245,7 +245,7 @@
    1.24        | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
    1.25  
    1.26      val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
    1.27 -      (cterm_of (sign_of thy) intr) (fn prems =>
    1.28 +      (cterm_of (Theory.sign_of thy) intr) (fn prems =>
    1.29         [(*insert prems and underlying sets*)
    1.30         cut_facts_tac prems 1,
    1.31         stac unfold 1,
    1.32 @@ -272,7 +272,7 @@
    1.33        map make_elim [Inl_inject, Inr_inject];
    1.34  
    1.35      val elims = map (fn t => prove_goalw_cterm rec_sets_defs
    1.36 -      (cterm_of (sign_of thy) t) (fn prems =>
    1.37 +      (cterm_of (Theory.sign_of thy) t) (fn prems =>
    1.38          [cut_facts_tac [hd prems] 1,
    1.39           dtac (unfold RS subst) 1,
    1.40           REPEAT (FIRSTGOAL (eresolve_tac rules1)),
    1.41 @@ -300,7 +300,7 @@
    1.42  
    1.43  (*String s should have the form t:Si where Si is an inductive set*)
    1.44  fun mk_cases elims s =
    1.45 -  let val prem = assume (read_cterm (sign_of_thm (hd elims)) (s, propT))
    1.46 +  let val prem = assume (read_cterm (Thm.sign_of_thm (hd elims)) (s, propT))
    1.47        fun mk_elim rl = rule_by_tactic (con_elim_tac (simpset())) (prem RS rl) 
    1.48  	               |> standard
    1.49    in case find_first is_some (map (try mk_elim) elims) of
    1.50 @@ -315,7 +315,7 @@
    1.51    let
    1.52      val _ = message "  Proving the induction rule...";
    1.53  
    1.54 -    val sign = sign_of thy;
    1.55 +    val sign = Theory.sign_of thy;
    1.56  
    1.57      val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
    1.58  
    1.59 @@ -387,8 +387,8 @@
    1.60      val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
    1.61      val setT = HOLogic.mk_setT sumT;
    1.62  
    1.63 -    val fp_name = if coind then Sign.intern_const (sign_of Gfp.thy) "gfp"
    1.64 -      else Sign.intern_const (sign_of Lfp.thy) "lfp";
    1.65 +    val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
    1.66 +      else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";
    1.67  
    1.68      val used = foldr add_term_names (intr_ts, []);
    1.69      val [sname, xname] = variantlist (["S", "x"], used);
    1.70 @@ -421,7 +421,7 @@
    1.71      (* add definiton of recursive sets to theory *)
    1.72  
    1.73      val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
    1.74 -    val full_rec_name = Sign.full_name (sign_of thy) rec_name;
    1.75 +    val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
    1.76  
    1.77      val rec_const = list_comb
    1.78        (Const (full_rec_name, paramTs ---> setT), params);
    1.79 @@ -538,7 +538,7 @@
    1.80      val _ = Theory.requires thy "Inductive"
    1.81        ((if coind then "co" else "") ^ "inductive definitions");
    1.82  
    1.83 -    val sign = sign_of thy;
    1.84 +    val sign = Theory.sign_of thy;
    1.85  
    1.86      (*parameters should agree for all mutually recursive components*)
    1.87      val (_, params) = strip_comb (hd cs);
    1.88 @@ -566,9 +566,9 @@
    1.89  
    1.90  fun add_inductive verbose coind c_strings intr_strings monos con_defs thy =
    1.91    let
    1.92 -    val sign = sign_of thy;
    1.93 -    val cs = map (readtm (sign_of thy) HOLogic.termTVar) c_strings;
    1.94 -    val intr_ts = map (readtm (sign_of thy) propT) intr_strings;
    1.95 +    val sign = Theory.sign_of thy;
    1.96 +    val cs = map (readtm (Theory.sign_of thy) HOLogic.termTVar) c_strings;
    1.97 +    val intr_ts = map (readtm (Theory.sign_of thy) propT) intr_strings;
    1.98  
    1.99      (* the following code ensures that each recursive set *)
   1.100      (* always has the same type in all introduction rules *)