# HG changeset patch # User wenzelm # Date 966614313 -7200 # Node ID f0cfddda603873ca02b3d422f7a166f3d7d12ebc # Parent 6f0b89f2a1f9153fa645c4ac3e6334f3203dde16 proper handling of defs; diff -r 6f0b89f2a1f9 -r f0cfddda6038 TFL/post.sml --- a/TFL/post.sml Fri Aug 18 17:53:49 2000 +0200 +++ b/TFL/post.sml Fri Aug 18 17:58:33 2000 +0200 @@ -185,11 +185,8 @@ (*Strip off the outer !P*) val spec'= read_instantiate [("x","P::?'b=>bool")] spec; - fun simplify_defn (ss, tflCongs) (thy,(id,pats)) = - let val dummy = deny (id mem (Sign.stamp_names_of (Theory.sign_of thy))) - ("Recursive definition " ^ id ^ - " would clash with the theory of the same name!") (* FIXME !? *) - val def = freezeT(get_def thy id) RS meta_eq_to_obj_eq + fun simplify_defn thy (ss, tflCongs) id pats def0 = + let val def = freezeT def0 RS meta_eq_to_obj_eq val {theory,rules,rows,TCs,full_pats_TCs} = Prim.post_definition (Prim.congs thy tflCongs) (thy, (def,pats)) @@ -216,9 +213,8 @@ *---------------------------------------------------------------------------*) fun define_i thy fid R ss_congs eqs = let val {functional,pats} = Prim.mk_functional thy eqs - val thy = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional - in (thy, simplify_defn ss_congs (thy, (fid, pats))) - end; + val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional + in (thy, simplify_defn thy ss_congs fid pats def) end; fun define thy fid R ss_congs seqs = define_i thy fid (read_term thy R) ss_congs (map (read_term thy) seqs) diff -r 6f0b89f2a1f9 -r f0cfddda6038 TFL/tfl.sig --- a/TFL/tfl.sig Fri Aug 18 17:53:49 2000 +0200 +++ b/TFL/tfl.sig Fri Aug 18 17:58:33 2000 +0200 @@ -25,7 +25,7 @@ -> {functional:term, pats: pattern list} - val wfrec_definition0 : theory -> string -> term -> term -> theory + val wfrec_definition0 : theory -> string -> term -> term -> theory * thm val post_definition : thm list -> theory * (thm * pattern list) -> {theory : theory, diff -r 6f0b89f2a1f9 -r f0cfddda6038 TFL/tfl.sml --- a/TFL/tfl.sml Fri Aug 18 17:53:49 2000 +0200 +++ b/TFL/tfl.sml Fri Aug 18 17:58:33 2000 +0200 @@ -439,7 +439,8 @@ (wfrec $ map_term_types poly_tvars R) $ functional val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M) - in #1 (PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy) end + val (thy', [def]) = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy + in (thy', def) end; end;