--- a/TFL/tfl.sml Mon Mar 13 13:27:44 2000 +0100
+++ b/TFL/tfl.sml Mon Mar 13 13:28:31 2000 +0100
@@ -381,7 +381,7 @@
(wfrec $ map_term_types poly_tvars R)
$ functional
val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M)
- in PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy end
+ in #1 (PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy) end
end;
@@ -534,11 +534,11 @@
val (Name,Ty) = dest_atom c
val defn = mk_const_def (Theory.sign_of thy)
(Name, Ty, S.list_mk_abs (args,rhs))
- val theory =
+ val (theory, [def0]) =
thy
|> PureThy.add_defs_i
[Thm.no_attributes (fid ^ "_def", defn)]
- val def = freezeT (get_thm theory (fid ^ "_def"))
+ val def = freezeT def0;
val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
else ()
(* val fconst = #lhs(S.dest_eq(concl def)) *)
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Mon Mar 13 13:27:44 2000 +0100
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Mon Mar 13 13:28:31 2000 +0100
@@ -360,7 +360,7 @@
(automaton_name ^ "_trans",
"(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
(automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
-|> (PureThy.add_defs o map Thm.no_attributes) (* old: Attributes.none *)
+|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))
[(automaton_name ^ "_initial_def",
automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
(automaton_name ^ "_asig_def",
@@ -401,7 +401,7 @@
Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
,NoSyn)]
-|> (PureThy.add_defs o map Thm.no_attributes)
+|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))
[(automaton_name ^ "_def",
automaton_name ^ " == " ^ comp_list)]
end)
@@ -416,7 +416,7 @@
thy
|> ContConsts.add_consts_i
[(automaton_name, auttyp,NoSyn)]
-|> (PureThy.add_defs o map Thm.no_attributes)
+|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))
[(automaton_name ^ "_def",
automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)]
end)
@@ -430,7 +430,7 @@
thy
|> ContConsts.add_consts_i
[(automaton_name, auttyp,NoSyn)]
-|> (PureThy.add_defs o map Thm.no_attributes)
+|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))
[(automaton_name ^ "_def",
automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)]
end)
@@ -462,7 +462,7 @@
Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
,NoSyn)]
-|> (PureThy.add_defs o map Thm.no_attributes)
+|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))
[(automaton_name ^ "_def",
automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
end)
--- a/src/HOLCF/domain/axioms.ML Mon Mar 13 13:27:44 2000 +0100
+++ b/src/HOLCF/domain/axioms.ML Mon Mar 13 13:28:31 2000 +0100
@@ -86,7 +86,7 @@
[take_def, finite_def])
end; (* let *)
-val add_axioms_i = PureThy.add_axioms_i o map Thm.no_attributes;
+fun add_axioms_i x = #1 o PureThy.add_axioms_i (map Thm.no_attributes x);
in (* local *)
--- a/src/HOLCF/domain/theorems.ML Mon Mar 13 13:27:44 2000 +0100
+++ b/src/HOLCF/domain/theorems.ML Mon Mar 13 13:28:31 2000 +0100
@@ -315,7 +315,7 @@
(filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
val copy_rews = copy_strict::copy_apps @ copy_stricts;
in thy |> Theory.add_path (Sign.base_name dname)
- |> (PureThy.add_thmss o map Thm.no_attributes) [
+ |> (#1 o (PureThy.add_thmss (map Thm.no_attributes [
("iso_rews" , iso_rews ),
("exhaust" , [exhaust] ),
("casedist" , [casedist]),
@@ -327,7 +327,7 @@
("dist_eqs", dist_eqs),
("inverts" , inverts ),
("injects" , injects ),
- ("copy_rews", copy_rews)]
+ ("copy_rews", copy_rews)])))
|> Theory.parent_path
end; (* let *)
@@ -590,13 +590,13 @@
in thy |> Theory.add_path comp_dnam
- |> (PureThy.add_thmss o map Thm.no_attributes) [
+ |> (#1 o (PureThy.add_thmss (map Thm.no_attributes [
("take_rews" , take_rews ),
("take_lemmas", take_lemmas),
("finites" , finites ),
("finite_ind", [finite_ind]),
("ind" , [ind ]),
- ("coind" , [coind ])]
+ ("coind" , [coind ])])))
|> Theory.parent_path
end; (* let *)
end; (* local *)
--- a/src/ZF/Tools/datatype_package.ML Mon Mar 13 13:27:44 2000 +0100
+++ b/src/ZF/Tools/datatype_package.ML Mon Mar 13 13:28:31 2000 +0100
@@ -245,10 +245,10 @@
if need_recursor then
thy |> Theory.add_consts_i
[(recursor_base_name, recursor_typ, NoSyn)]
- |> PureThy.add_defs_i [Thm.no_attributes recursor_def]
+ |> (#1 o PureThy.add_defs_i [Thm.no_attributes recursor_def])
else thy;
- val thy0 = thy_path
+ val (thy0, con_defs) = thy_path
|> Theory.add_consts_i
((case_base_name, case_typ, NoSyn) ::
map #1 (flat con_ty_lists))
@@ -257,11 +257,8 @@
(case_def ::
flat (ListPair.map mk_con_defs
(1 upto npart, con_ty_lists))))
- |> add_recursor
- |> Theory.parent_path
-
- val con_defs = get_def thy0 case_name ::
- map (get_def thy0 o #2) (flat con_ty_lists);
+ |>> add_recursor
+ |>> Theory.parent_path
val (thy1, ind_result) =
thy0 |> Ind_Package.add_inductive_i
@@ -390,12 +387,12 @@
in
(*Updating theory components: simprules and datatype info*)
(thy1 |> Theory.add_path big_rec_base_name
- |> PureThy.add_thmss [(("simps", simps),
- [Simplifier.simp_add_global])]
- |> PureThy.add_thmss [(("", intrs),
+ |> (#1 o PureThy.add_thmss [(("simps", simps),
+ [Simplifier.simp_add_global])])
+ |> (#1 o PureThy.add_thmss [(("", intrs),
(*not "intrs" to avoid the warning that they
are already stored by the inductive package*)
- [Classical.safe_intro_global])]
+ [Classical.safe_intro_global])])
|> DatatypesData.put
(Symtab.update
((big_rec_name, dt_info), DatatypesData.get thy1))
--- a/src/ZF/Tools/induct_tacs.ML Mon Mar 13 13:27:44 2000 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Mon Mar 13 13:28:31 2000 +0100
@@ -175,7 +175,7 @@
in
thy |> Theory.add_path (Sign.base_name big_rec_name)
- |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
+ |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
|> DatatypesData.put
(Symtab.update
((big_rec_name, dt_info), DatatypesData.get thy))
--- a/src/ZF/Tools/inductive_package.ML Mon Mar 13 13:27:44 2000 +0100
+++ b/src/ZF/Tools/inductive_package.ML Mon Mar 13 13:28:31 2000 +0100
@@ -182,7 +182,7 @@
(*add definitions of the inductive sets*)
val thy1 = thy |> Theory.add_path big_rec_base_name
- |> PureThy.add_defs_i (map Thm.no_attributes axpairs)
+ |> (#1 o PureThy.add_defs_i (map Thm.no_attributes axpairs))
(*fetch fp definitions from the theory*)
@@ -531,12 +531,10 @@
val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0)
|> standard
and mutual_induct = CP.remove_split mutual_induct_fsplit
- in
- (thy
- |> PureThy.add_thms
- [(("induct", induct), []),
- (("mutual_induct", mutual_induct), [])],
- induct, mutual_induct)
+
+ val (thy', [induct', mutual_induct']) =
+ thy |> PureThy.add_thms [(("induct", induct), []), (("mutual_induct", mutual_induct), [])];
+ in (thy', induct', mutual_induct')
end; (*of induction_rules*)
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
@@ -546,26 +544,28 @@
else (thy1, raw_induct, TrueI)
and defs = big_rec_def :: part_rec_defs
- in
- (thy2
- |> (PureThy.add_thms o map Thm.no_attributes)
- [("bnd_mono", bnd_mono),
- ("dom_subset", dom_subset),
- ("elim", elim)]
- |> (PureThy.add_thmss o map Thm.no_attributes)
- [("defs", defs),
- ("intrs", intrs)]
- |> Theory.parent_path,
- {defs = defs,
- bnd_mono = bnd_mono,
- dom_subset = dom_subset,
- intrs = intrs,
- elim = elim,
- mk_cases = mk_cases,
- induct = induct,
- mutual_induct = mutual_induct})
- end;
+ val (thy3, ([bnd_mono', dom_subset', elim'], [defs', intrs'])) =
+ thy2
+ |> (PureThy.add_thms o map Thm.no_attributes)
+ [("bnd_mono", bnd_mono),
+ ("dom_subset", dom_subset),
+ ("elim", elim)]
+ |>>> (PureThy.add_thmss o map Thm.no_attributes)
+ [("defs", defs),
+ ("intrs", intrs)]
+ |>> Theory.parent_path;
+ in
+ (thy3,
+ {defs = defs',
+ bnd_mono = bnd_mono',
+ dom_subset = dom_subset',
+ intrs = intrs',
+ elim = elim',
+ mk_cases = mk_cases,
+ induct = induct,
+ mutual_induct = mutual_induct})
+ end;
(*external version, accepting strings*)
--- a/src/ZF/Tools/primrec_package.ML Mon Mar 13 13:27:44 2000 +0100
+++ b/src/ZF/Tools/primrec_package.ML Mon Mar 13 13:28:31 2000 +0100
@@ -167,10 +167,9 @@
val Some (fname, ftype, ls, rs, con_info, eqns) =
foldr (process_eqn thy) (map snd recursion_eqns, None);
val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns)
- val thy' = thy |> Theory.add_path (Sign.base_name (#1 def))
+ val (thy', [def_thm]) = thy |> Theory.add_path (Sign.base_name (#1 def))
|> (PureThy.add_defs_i o map Thm.no_attributes) [def]
- val rewrites = get_thm thy' (#1 def) ::
- map mk_meta_eq (#rec_rewrites con_info)
+ val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
val char_thms =
(if !Ind_Syntax.trace then (* FIXME message / quiet_mode (!?) *)
writeln ("Proving equations for primrec function " ^ fname)
@@ -183,9 +182,9 @@
recursion_eqns);
val simps = char_thms;
val thy'' = thy'
- |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
- |> PureThy.add_thms (map (rpair [])
- (filter_out (equal "_" o fst) (map fst recursion_eqns ~~ simps)))
+ |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
+ |> (#1 o PureThy.add_thms (map (rpair [])
+ (filter_out (equal "_" o fst) (map fst recursion_eqns ~~ simps))))
|> Theory.parent_path;
in
(thy'', char_thms)