eliminated tthm type and Attribute structure;
authorwenzelm
Tue Jan 12 13:54:51 1999 +0100 (1999-01-12 ago)
changeset 6092d9db67970c73
parent 6091 e3cdbd929a24
child 6093 87bf8c03b169
eliminated tthm type and Attribute structure;
TFL/tfl.sml
src/HOL/HOL.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/typedef_package.ML
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/theorems.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/TFL/tfl.sml	Tue Jan 12 13:40:08 1999 +0100
     1.2 +++ b/TFL/tfl.sml	Tue Jan 12 13:54:51 1999 +0100
     1.3 @@ -339,7 +339,7 @@
     1.4  	 Sign.infer_types (sign_of thy) (K None) (K None) [] false
     1.5  	       ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], 
     1.6  		propT)
     1.7 -  in  PureThy.add_defs_i [Attribute.none (def_name, def_term)] thy  end
     1.8 +  in  PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy  end
     1.9  end;
    1.10  
    1.11  
    1.12 @@ -461,7 +461,7 @@
    1.13       val R'abs = S.rand R'
    1.14       val theory =
    1.15         thy
    1.16 -       |> PureThy.add_defs_i [Attribute.none (Name ^ "_def", subst_free[(R1,R')] proto_def)];
    1.17 +       |> PureThy.add_defs_i [Thm.no_attributes (Name ^ "_def", subst_free[(R1,R')] proto_def)];
    1.18       val def = freezeT((get_axiom theory (Name ^ "_def")) RS meta_eq_to_obj_eq)
    1.19       val fconst = #lhs(S.dest_eq(concl def)) 
    1.20       val tych = Thry.typecheck theory
     2.1 --- a/src/HOL/HOL.ML	Tue Jan 12 13:40:08 1999 +0100
     2.2 +++ b/src/HOL/HOL.ML	Tue Jan 12 13:54:51 1999 +0100
     2.3 @@ -422,7 +422,7 @@
     2.4  
     2.5  local
     2.6  
     2.7 -fun gen_rulify x = Attrib.no_args (Attribute.rule (K (normalize_thm [RSspec, RSmp]))) x;
     2.8 +fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x;
     2.9  
    2.10  in
    2.11  
     3.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Jan 12 13:40:08 1999 +0100
     3.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Jan 12 13:54:51 1999 +0100
     3.3 @@ -275,7 +275,7 @@
     3.4  
     3.5    in
     3.6      (thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
     3.7 -             PureThy.add_tthmss [(("recs", Attribute.tthms_of rec_thms), [])] |>
     3.8 +             PureThy.add_thmss [(("recs", rec_thms), [])] |>
     3.9               Theory.parent_path,
    3.10       reccomb_names, rec_thms)
    3.11    end;
    3.12 @@ -518,7 +518,7 @@
    3.13  
    3.14    in
    3.15      (thy' |> Theory.add_path big_name |>
    3.16 -             PureThy.add_tthmss [(("size", Attribute.tthms_of size_thms), [])] |>
    3.17 +             PureThy.add_thmss [(("size", size_thms), [])] |>
    3.18               Theory.parent_path,
    3.19       size_thms)
    3.20    end;
     4.1 --- a/src/HOL/Tools/datatype_aux.ML	Tue Jan 12 13:40:08 1999 +0100
     4.2 +++ b/src/HOL/Tools/datatype_aux.ML	Tue Jan 12 13:54:51 1999 +0100
     4.3 @@ -78,14 +78,14 @@
     4.4  fun store_thmss label tnames thmss thy =
     4.5    foldr (fn ((tname, thms), thy') => thy' |>
     4.6      Theory.add_path tname |>
     4.7 -    PureThy.add_tthmss [((label, Attribute.tthms_of thms), [])] |>
     4.8 +    PureThy.add_thmss [((label, thms), [])] |>
     4.9      Theory.parent_path)
    4.10        (tnames ~~ thmss, thy);
    4.11  
    4.12  fun store_thms label tnames thms thy =
    4.13    foldr (fn ((tname, thm), thy') => thy' |>
    4.14      Theory.add_path tname |>
    4.15 -    PureThy.add_tthms [((label, Attribute.tthm_of thm), [])] |>
    4.16 +    PureThy.add_thms [((label, thm), [])] |>
    4.17      Theory.parent_path)
    4.18        (tnames ~~ thms, thy);
    4.19  
     5.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jan 12 13:40:08 1999 +0100
     5.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jan 12 13:54:51 1999 +0100
     5.3 @@ -402,7 +402,7 @@
     5.4  
     5.5      val thy11 = thy10 |>
     5.6        Theory.add_path (space_implode "_" new_type_names) |>
     5.7 -      PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |>
     5.8 +      PureThy.add_thmss [(("simps", simps), [])] |>
     5.9        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    5.10        Theory.parent_path;
    5.11  
    5.12 @@ -459,7 +459,7 @@
    5.13  
    5.14      val thy11 = thy10 |>
    5.15        Theory.add_path (space_implode "_" new_type_names) |>
    5.16 -      PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |>
    5.17 +      PureThy.add_thmss [(("simps", simps), [])] |>
    5.18        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    5.19        Theory.parent_path;
    5.20  
    5.21 @@ -550,7 +550,7 @@
    5.22  
    5.23      val thy9 = thy8 |>
    5.24        Theory.add_path (space_implode "_" new_type_names) |>
    5.25 -      PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |>
    5.26 +      PureThy.add_thmss [(("simps", simps), [])] |>
    5.27        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    5.28        Theory.parent_path;
    5.29  
    5.30 @@ -571,8 +571,7 @@
    5.31        simps = simps})
    5.32    end;
    5.33  
    5.34 -val rep_datatype = gen_rep_datatype
    5.35 -  (fn thy => Attribute.thms_of o PureThy.get_tthmss thy) get_thm;
    5.36 +val rep_datatype = gen_rep_datatype (fn thy => PureThy.get_thmss thy) get_thm;
    5.37  val rep_datatype_i = gen_rep_datatype (K I) (K I);
    5.38  
    5.39  (******************************** add datatype ********************************)
     6.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jan 12 13:40:08 1999 +0100
     6.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jan 12 13:54:51 1999 +0100
     6.3 @@ -535,7 +535,7 @@
     6.4  
     6.5      val thy7 = thy6 |>
     6.6        Theory.add_path big_name |>
     6.7 -      PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] |>
     6.8 +      PureThy.add_thms [(("induct", dt_induct), [])] |>
     6.9        Theory.parent_path;
    6.10  
    6.11    in (thy7, constr_inject, dist_rewrites, dt_induct)
     7.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Jan 12 13:40:08 1999 +0100
     7.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Jan 12 13:54:51 1999 +0100
     7.3 @@ -464,12 +464,11 @@
     7.4        else standard (raw_induct RSN (2, rev_mp));
     7.5  
     7.6      val thy'' = thy' |>
     7.7 -      PureThy.add_tthmss [(("intrs", Attribute.tthms_of intrs), [])] |>
     7.8 -      (if no_elim then I else PureThy.add_tthmss
     7.9 -        [(("elims", Attribute.tthms_of elims), [])]) |>
    7.10 -      (if no_ind then I else PureThy.add_tthms
    7.11 -        [(((if coind then "co" else "") ^ "induct",
    7.12 -          Attribute.tthm_of induct), [])]) |>
    7.13 +      PureThy.add_thmss [(("intrs", intrs), [])] |>
    7.14 +      (if no_elim then I else PureThy.add_thmss
    7.15 +        [(("elims", elims), [])]) |>
    7.16 +      (if no_ind then I else PureThy.add_thms
    7.17 +        [(((if coind then "co" else "") ^ "induct", induct), [])]) |>
    7.18        Theory.parent_path;
    7.19  
    7.20    in (thy'',
    7.21 @@ -517,7 +516,7 @@
    7.22  
    7.23      val thy'' = thy' |>
    7.24        (if coind then I
    7.25 -       else PureThy.add_tthms [(("induct", Attribute.tthm_of induct), [])]) |>
    7.26 +       else PureThy.add_thms [(("induct", induct), [])]) |>
    7.27        Theory.parent_path
    7.28  
    7.29    in (thy'',
    7.30 @@ -600,8 +599,8 @@
    7.31      val intr_ts'' = map subst intr_ts';
    7.32  
    7.33    in add_inductive_i verbose false "" coind false false cs'' intr_ts''
    7.34 -    (Attribute.thms_of (PureThy.get_tthmss thy monos))
    7.35 -    (Attribute.thms_of (PureThy.get_tthmss thy con_defs)) thy
    7.36 +    (PureThy.get_thmss thy monos)
    7.37 +    (PureThy.get_thmss thy con_defs) thy
    7.38    end;
    7.39  
    7.40  end;
     8.1 --- a/src/HOL/Tools/primrec_package.ML	Tue Jan 12 13:40:08 1999 +0100
     8.2 +++ b/src/HOL/Tools/primrec_package.ML	Tue Jan 12 13:54:51 1999 +0100
     8.3 @@ -235,11 +235,11 @@
     8.4        commas names1 ^ " ...");
     8.5      val char_thms = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (sign_of thy') t)
     8.6          (fn _ => [rtac refl 1])) eqns;
     8.7 -    val tsimps = Attribute.tthms_of char_thms;
     8.8 +    val simps = char_thms;
     8.9      val thy'' = thy' |>
    8.10 -      PureThy.add_tthmss [(("simps", tsimps), [Simplifier.simp_add_global])] |>
    8.11 -      PureThy.add_tthms (map (rpair [])
    8.12 -         (filter_out (equal "" o fst) (map fst eqns ~~ tsimps))) |>
    8.13 +      PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])] |>
    8.14 +      PureThy.add_thms (map (rpair [])
    8.15 +        (filter_out (equal "" o fst) (map fst eqns ~~ simps))) |>
    8.16        Theory.parent_path;
    8.17    in
    8.18      (thy'', char_thms)
     9.1 --- a/src/HOL/Tools/record_package.ML	Tue Jan 12 13:40:08 1999 +0100
     9.2 +++ b/src/HOL/Tools/record_package.ML	Tue Jan 12 13:54:51 1999 +0100
     9.3 @@ -53,7 +53,7 @@
     9.4    let
     9.5      val ss = Simplifier.simpset_ref_of thy;
     9.6      val cs = Classical.claset_ref_of thy;
     9.7 -    val (cs', ss') = (! cs, ! ss) addIffs [Attribute.thm_of th];
     9.8 +    val (cs', ss') = (! cs, ! ss) addIffs [th];
     9.9    in ss := ss'; cs := cs'; (thy, th) end;
    9.10  
    9.11  fun add_wrapper wrapper thy =
    9.12 @@ -68,7 +68,7 @@
    9.13  val (op :==) = Logic.mk_defpair;
    9.14  val (op ===) = HOLogic.mk_Trueprop o HOLogic.mk_eq;
    9.15  
    9.16 -fun get_defs thy specs = map (PureThy.get_tthm thy o fst) specs;
    9.17 +fun get_defs thy specs = map (PureThy.get_thm thy o fst) specs;
    9.18  
    9.19  
    9.20  (* proof by simplification *)
    9.21 @@ -76,14 +76,13 @@
    9.22  fun prove_simp thy tacs simps =
    9.23    let
    9.24      val sign = Theory.sign_of thy;
    9.25 -    val ss = Simplifier.addsimps (HOL_basic_ss, Attribute.thms_of simps);
    9.26 +    val ss = Simplifier.addsimps (HOL_basic_ss, simps);
    9.27  
    9.28      fun prove goal =
    9.29 -      Attribute.tthm_of
    9.30 -        (Goals.prove_goalw_cterm [] (Thm.cterm_of sign goal)
    9.31 -          (K (tacs @ [ALLGOALS (Simplifier.simp_tac ss)]))
    9.32 -        handle ERROR => error ("The error(s) above occurred while trying to prove "
    9.33 -          ^ quote (Sign.string_of_term sign goal)));
    9.34 +      Goals.prove_goalw_cterm [] (Thm.cterm_of sign goal)
    9.35 +        (K (tacs @ [ALLGOALS (Simplifier.simp_tac ss)]))
    9.36 +      handle ERROR => error ("The error(s) above occurred while trying to prove "
    9.37 +        ^ quote (Sign.string_of_term sign goal));
    9.38    in prove end;
    9.39  
    9.40  
    9.41 @@ -328,12 +327,12 @@
    9.42   {args: (string * sort) list,
    9.43    parent: (typ list * string) option,
    9.44    fields: (string * typ) list,
    9.45 -  simps: tthm list};
    9.46 +  simps: thm list};
    9.47  
    9.48  type parent_info =
    9.49   {name: string,
    9.50    fields: (string * typ) list,
    9.51 -  simps: tthm list};
    9.52 +  simps: thm list};
    9.53  
    9.54  
    9.55  (* data kind 'HOL/records' *)
    9.56 @@ -519,12 +518,10 @@
    9.57  
    9.58      (* 1st stage: types_thy *)
    9.59  
    9.60 -    val (types_thy, simps) =
    9.61 +    val (types_thy, datatype_simps) =
    9.62        thy
    9.63        |> field_type_defs fieldT_specs;
    9.64  
    9.65 -    val datatype_simps = Attribute.tthms_of simps;
    9.66 -
    9.67  
    9.68      (* 2nd stage: defs_thy *)
    9.69  
    9.70 @@ -532,7 +529,7 @@
    9.71        types_thy
    9.72         |> (Theory.add_consts_i o map (Syntax.no_syn o apfst base))
    9.73           (field_decls @ dest_decls)
    9.74 -       |> (PureThy.add_defs_i o map (fn x => (x, [Attribute.tag_internal])))
    9.75 +       |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal])))
    9.76           (field_specs @ dest_specs);
    9.77  
    9.78      val field_defs = get_defs defs_thy field_specs;
    9.79 @@ -547,14 +544,14 @@
    9.80      val field_injects = map prove_std inject_props;
    9.81      val dest_convs = map prove_std dest_props;
    9.82      val surj_pairs = map (prove [DatatypePackage.induct_tac "p" 1]
    9.83 -      (map (apfst Thm.symmetric) field_defs @ dest_convs)) surj_props;
    9.84 +      (map Thm.symmetric field_defs @ dest_convs)) surj_props;
    9.85  
    9.86      fun mk_split th = SplitPairedAll.rule (th RS eq_reflection);
    9.87 -    val field_splits = map (fn (th, _) => Attribute.tthm_of (mk_split th)) surj_pairs;
    9.88 +    val field_splits = map mk_split surj_pairs;
    9.89  
    9.90      val thms_thy =
    9.91        defs_thy
    9.92 -      |> (PureThy.add_tthmss o map Attribute.none)
    9.93 +      |> (PureThy.add_thmss o map Thm.no_attributes)
    9.94          [("field_defs", field_defs),
    9.95            ("dest_defs", dest_defs),
    9.96            ("dest_convs", dest_convs),
    9.97 @@ -692,7 +689,7 @@
    9.98        |> Theory.add_path bname
    9.99        |> field_definitions fields names zeta moreT more vars named_vars;
   9.100  
   9.101 -    val named_splits = map2 (fn (c, (th, _)) => (suffix field_typeN c, th)) (names, field_splits);
   9.102 +    val named_splits = map2 (fn (c, th) => (suffix field_typeN c, th)) (names, field_splits);
   9.103  
   9.104  
   9.105      (* 2nd stage: defs_thy *)
   9.106 @@ -705,9 +702,9 @@
   9.107        |> Theory.add_trfuns ([], [], field_tr's, [])
   9.108        |> (Theory.add_consts_i o map Syntax.no_syn)
   9.109          (sel_decls @ update_decls @ make_decls)
   9.110 -      |> (PureThy.add_defs_i o map (fn x => (x, [Attribute.tag_internal])))
   9.111 +      |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal])))
   9.112          (sel_specs @ update_specs)
   9.113 -      |> (PureThy.add_defs_i o map Attribute.none) make_specs;
   9.114 +      |> (PureThy.add_defs_i o map Thm.no_attributes) make_specs;
   9.115  
   9.116      val sel_defs = get_defs defs_thy sel_specs;
   9.117      val update_defs = get_defs defs_thy update_specs;
   9.118 @@ -726,13 +723,13 @@
   9.119  
   9.120      val thms_thy =
   9.121        defs_thy
   9.122 -      |> (PureThy.add_tthmss o map Attribute.none)
   9.123 +      |> (PureThy.add_thmss o map Thm.no_attributes)
   9.124          [("select_defs", sel_defs),
   9.125            ("update_defs", update_defs),
   9.126            ("make_defs", make_defs),
   9.127            ("select_convs", sel_convs),
   9.128            ("update_convs", update_convs)]
   9.129 -      |> PureThy.add_tthmss
   9.130 +      |> PureThy.add_thmss
   9.131          [(("simps", simps), [Simplifier.simp_add_global]),
   9.132           (("iffs", field_injects), [add_iffs_global])];
   9.133  
    10.1 --- a/src/HOL/Tools/typedef_package.ML	Tue Jan 12 13:40:08 1999 +0100
    10.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue Jan 12 13:54:51 1999 +0100
    10.3 @@ -141,9 +141,9 @@
    10.4       ((if no_def then [] else [(name, setT, NoSyn)]) @
    10.5        [(Rep_name, newT --> oldT, NoSyn),
    10.6         (Abs_name, oldT --> newT, NoSyn)])
    10.7 -    |> (if no_def then I else (PureThy.add_defs_i o map Attribute.none)
    10.8 +    |> (if no_def then I else (PureThy.add_defs_i o map Thm.no_attributes)
    10.9       [(name ^ "_def", Logic.mk_equals (setC, set))])
   10.10 -    |> (PureThy.add_axioms_i o map Attribute.none)
   10.11 +    |> (PureThy.add_axioms_i o map Thm.no_attributes)
   10.12       [(Rep_name, rep_type),
   10.13        (Rep_name ^ "_inverse", rep_type_inv),
   10.14        (Abs_name ^ "_inverse", abs_type_inv)]
    11.1 --- a/src/HOLCF/domain/axioms.ML	Tue Jan 12 13:40:08 1999 +0100
    11.2 +++ b/src/HOLCF/domain/axioms.ML	Tue Jan 12 13:54:51 1999 +0100
    11.3 @@ -86,7 +86,7 @@
    11.4      [take_def, finite_def])
    11.5  end; (* let *)
    11.6  
    11.7 -val add_axioms_i = PureThy.add_axioms_i o map Attribute.none;
    11.8 +val add_axioms_i = PureThy.add_axioms_i o map Thm.no_attributes;
    11.9  
   11.10  in (* local *)
   11.11  
    12.1 --- a/src/HOLCF/domain/theorems.ML	Tue Jan 12 13:40:08 1999 +0100
    12.2 +++ b/src/HOLCF/domain/theorems.ML	Tue Jan 12 13:54:51 1999 +0100
    12.3 @@ -323,7 +323,7 @@
    12.4                          (filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
    12.5  val copy_rews = copy_strict::copy_apps @ copy_stricts;
    12.6  in thy |> Theory.add_path (Sign.base_name dname)
    12.7 -       |> (PureThy.add_tthmss o map Attribute.no_attrss) [
    12.8 +       |> (PureThy.add_thmss o map Thm.no_attributes) [
    12.9  		("iso_rews" , iso_rews  ),
   12.10  		("exhaust"  , [exhaust] ),
   12.11  		("casedist" , [casedist]),
   12.12 @@ -598,7 +598,7 @@
   12.13  
   12.14  
   12.15  in thy |> Theory.add_path comp_dnam
   12.16 -       |> (PureThy.add_tthmss o map Attribute.no_attrss) [
   12.17 +       |> (PureThy.add_thmss o map Thm.no_attributes) [
   12.18  		("take_rews"  , take_rews  ),
   12.19  		("take_lemmas", take_lemmas),
   12.20  		("finites"    , finites    ),
    13.1 --- a/src/ZF/Tools/datatype_package.ML	Tue Jan 12 13:40:08 1999 +0100
    13.2 +++ b/src/ZF/Tools/datatype_package.ML	Tue Jan 12 13:54:51 1999 +0100
    13.3 @@ -245,7 +245,7 @@
    13.4        if need_recursor then
    13.5  	   thy |> Theory.add_consts_i 
    13.6  	            [(recursor_base_name, recursor_typ, NoSyn)]
    13.7 -	       |> PureThy.add_defs_i [Attribute.none recursor_def]
    13.8 +	       |> PureThy.add_defs_i [Thm.no_attributes recursor_def]
    13.9        else thy;
   13.10  
   13.11    val thy0 = thy_path
   13.12 @@ -253,7 +253,7 @@
   13.13  		 ((case_base_name, case_typ, NoSyn) ::
   13.14  		  map #1 (flat con_ty_lists))
   13.15  	     |> PureThy.add_defs_i
   13.16 -		 (map Attribute.none 
   13.17 +		 (map Thm.no_attributes
   13.18  		  (case_def :: 
   13.19  		   flat (ListPair.map mk_con_defs
   13.20  			 (1 upto npart, con_ty_lists))))
   13.21 @@ -392,8 +392,7 @@
   13.22   in
   13.23    (*Updating theory components: simprules and datatype info*)
   13.24    (thy1 |> Theory.add_path big_rec_base_name
   13.25 -        |> PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), 
   13.26 -				[Simplifier.simp_add_global])] 
   13.27 +        |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
   13.28          |> DatatypesData.put 
   13.29  	    (Symtab.update
   13.30  	     ((big_rec_name, dt_info), DatatypesData.get thy1)) 
    14.1 --- a/src/ZF/Tools/induct_tacs.ML	Tue Jan 12 13:40:08 1999 +0100
    14.2 +++ b/src/ZF/Tools/induct_tacs.ML	Tue Jan 12 13:54:51 1999 +0100
    14.3 @@ -165,8 +165,7 @@
    14.4  
    14.5    in
    14.6        thy |> Theory.add_path (Sign.base_name big_rec_name)
    14.7 -	  |> PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), 
    14.8 -				  [Simplifier.simp_add_global])] 
    14.9 +	  |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
   14.10  	  |> DatatypesData.put 
   14.11  	      (Symtab.update
   14.12  	       ((big_rec_name, dt_info), DatatypesData.get thy)) 
    15.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Jan 12 13:40:08 1999 +0100
    15.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Jan 12 13:54:51 1999 +0100
    15.3 @@ -169,7 +169,7 @@
    15.4  
    15.5    (*add definitions of the inductive sets*)
    15.6    val thy1 = thy |> Theory.add_path big_rec_base_name
    15.7 -                 |> PureThy.add_defs_i (map Attribute.none axpairs)  
    15.8 +                 |> PureThy.add_defs_i (map Thm.no_attributes axpairs)  
    15.9  
   15.10  
   15.11    (*fetch fp definitions from the theory*)
   15.12 @@ -519,9 +519,9 @@
   15.13       and mutual_induct = CP.remove_split mutual_induct_fsplit
   15.14      in
   15.15        (thy
   15.16 -	|> PureThy.add_tthms 
   15.17 -	    [(("induct", Attribute.tthm_of induct), []),
   15.18 -	     (("mutual_induct", Attribute.tthm_of mutual_induct), [])],
   15.19 +	|> PureThy.add_thms 
   15.20 +	    [(("induct", induct), []),
   15.21 +	     (("mutual_induct", mutual_induct), [])],
   15.22         induct, mutual_induct)
   15.23      end;  (*of induction_rules*)
   15.24  
   15.25 @@ -534,13 +534,13 @@
   15.26  
   15.27   in
   15.28     (thy2
   15.29 -	 |> PureThy.add_tthms
   15.30 -	      [(("bnd_mono", Attribute.tthm_of bnd_mono), []),
   15.31 -	       (("dom_subset", Attribute.tthm_of dom_subset), []),
   15.32 -	       (("elim", Attribute.tthm_of elim), [])]
   15.33 -	 |> PureThy.add_tthmss
   15.34 -	       [(("defs", Attribute.tthms_of defs), []),
   15.35 -		(("intrs", Attribute.tthms_of intrs), [])]
   15.36 +	 |> (PureThy.add_thms o map Thm.no_attributes)
   15.37 +	      [("bnd_mono", bnd_mono),
   15.38 +	       ("dom_subset", dom_subset),
   15.39 +	       ("elim", elim)]
   15.40 +	 |> (PureThy.add_thmss o map Thm.no_attributes)
   15.41 +	       [("defs", defs),
   15.42 +		("intrs", intrs)]
   15.43           |> Theory.parent_path,
   15.44      {defs = defs,
   15.45       bnd_mono = bnd_mono,
    16.1 --- a/src/ZF/Tools/primrec_package.ML	Tue Jan 12 13:40:08 1999 +0100
    16.2 +++ b/src/ZF/Tools/primrec_package.ML	Tue Jan 12 13:54:51 1999 +0100
    16.3 @@ -173,20 +173,20 @@
    16.4      val rewrites = get_axiom thy' (#1 def) ::
    16.5  	           map mk_meta_eq (#rec_rewrites con_info)
    16.6      val char_thms = 
    16.7 -	(if !Ind_Syntax.trace then
    16.8 +	(if !Ind_Syntax.trace then	(* FIXME message / quiet_mode (!?) *)
    16.9  	     writeln ("Proving equations for primrec function " ^ fname)
   16.10  	 else ();
   16.11 -	 map (fn (_,t) => 
   16.12 +	 map (fn (_,t) =>
   16.13  	      prove_goalw_cterm rewrites
   16.14  		(Ind_Syntax.traceIt "next primrec equation = "
   16.15  		 (cterm_of (sign_of thy') t))
   16.16  	      (fn _ => [rtac refl 1]))
   16.17  	 recursion_eqns);
   16.18 -    val tsimps = Attribute.tthms_of char_thms;
   16.19 +    val simps = char_thms;
   16.20      val thy'' = thy' 
   16.21 -      |> PureThy.add_tthmss [(("simps", tsimps), [Simplifier.simp_add_global])]
   16.22 -      |> PureThy.add_tthms (map (rpair [])
   16.23 -         (filter_out (equal "_" o fst) (map fst recursion_eqns ~~ tsimps)))
   16.24 +      |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
   16.25 +      |> PureThy.add_thms (map (rpair [])
   16.26 +         (filter_out (equal "_" o fst) (map fst recursion_eqns ~~ simps)))
   16.27        |> Theory.parent_path;
   16.28    in
   16.29      (thy'', char_thms)