# HG changeset patch # User huffman # Date 1133308744 -3600 # Node ID 9ca223aedb1e661405416c78fb0d1fe88156b435 # Parent 4afdf02d9831007c13fba641308eb71c46c98dd0 add definitions as defs, not axioms diff -r 4afdf02d9831 -r 9ca223aedb1e src/HOLCF/domain/axioms.ML --- a/src/HOLCF/domain/axioms.ML Wed Nov 30 00:56:01 2005 +0100 +++ b/src/HOLCF/domain/axioms.ML Wed Nov 30 00:59:04 2005 +0100 @@ -114,6 +114,9 @@ fun add_axioms_i x = #1 o PureThy.add_axioms_i (map Thm.no_attributes x); fun add_axioms_infer axms thy = add_axioms_i (infer_types thy axms) thy; +fun add_defs_i x = #1 o (PureThy.add_defs_i false) (map Thm.no_attributes x); +fun add_defs_infer defs thy = add_defs_i (infer_types thy defs) thy; + in (* local *) fun add_axioms (comp_dnam, eqs : eq list) thy' = let @@ -154,12 +157,12 @@ in foldr1 mk_conj (mapn one_comp 0 eqs)end )); fun add_one (thy,(dnam,axs,dfs)) = thy |> Theory.add_path dnam - |> add_axioms_infer dfs(*add_defs_i*) + |> add_defs_infer dfs |> add_axioms_infer axs |> Theory.parent_path; val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); in thy |> Theory.add_path comp_dnam - |> add_axioms_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) + |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) |> Theory.parent_path end;