# HG changeset patch # User wenzelm # Date 952950511 -3600 # Node ID b8389b4fca9c42230145c3b75a0a0d04d45d38be # Parent 258281c43deae7e870d0ef6a462cacb68ec8cec6 adapted to new PureThy.add_thms etc.; diff -r 258281c43dea -r b8389b4fca9c TFL/tfl.sml --- 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)) *) diff -r 258281c43dea -r b8389b4fca9c src/HOLCF/IOA/meta_theory/ioa_package.ML --- 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) diff -r 258281c43dea -r b8389b4fca9c src/HOLCF/domain/axioms.ML --- 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 *) diff -r 258281c43dea -r b8389b4fca9c src/HOLCF/domain/theorems.ML --- 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 *) diff -r 258281c43dea -r b8389b4fca9c src/ZF/Tools/datatype_package.ML --- 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)) diff -r 258281c43dea -r b8389b4fca9c src/ZF/Tools/induct_tacs.ML --- 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)) diff -r 258281c43dea -r b8389b4fca9c src/ZF/Tools/inductive_package.ML --- 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*) diff -r 258281c43dea -r b8389b4fca9c src/ZF/Tools/primrec_package.ML --- 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)