add function add_qualified_def

--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Mar 08 15:00:34 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Mon Mar 08 07:22:30 2010 -0800
@@ -168,6 +168,13 @@
     ((const, def_thm), thy)
   end;
 
+fun add_qualified_def name (path, eqn) thy =
+    thy
+    |> Sign.add_path path
+    |> yield_singleton (PureThy.add_defs false)
+        (Thm.no_attributes (Binding.name name, eqn))
+    ||> Sign.parent_path;
+
 fun add_qualified_thm name (path, thm) thy =
     thy
     |> Sign.add_path path
@@ -239,12 +246,8 @@
           Sign.declare_const ((take_bind, take_type), NoSyn) thy;
         val take_eqn = Logic.mk_equals (take_const, take_rhs);
         val (take_def_thm, thy) =
-          thy
-          |> Sign.add_path (Binding.name_of tbind)
-          |> yield_singleton
-              (PureThy.add_defs false o map Thm.no_attributes)
-              (Binding.name "take_def", take_eqn)
-          ||> Sign.parent_path;
+            add_qualified_def "take_def"
+             (Binding.name_of tbind, take_eqn) thy;
       in ((take_const, take_def_thm), thy) end;
     val ((take_consts, take_defs), thy) = thy
       |> fold_map define_take_const (dom_binds ~~ take_rhss ~~ dom_eqns)
@@ -388,12 +391,8 @@
             (lambda n (mk_eq (mk_capply (take_const $ n, x), x))));
         val finite_eqn = Logic.mk_equals (finite_const, finite_rhs);
         val (finite_def_thm, thy) =
-          thy
-          |> Sign.add_path (Binding.name_of tbind)
-          |> yield_singleton
-              (PureThy.add_defs false o map Thm.no_attributes)
-              (Binding.name "finite_def", finite_eqn)
-          ||> Sign.parent_path;
+            add_qualified_def "finite_def"
+             (Binding.name_of tbind, finite_eqn) thy;
       in ((finite_const, finite_def_thm), thy) end;
     val ((finite_consts, finite_defs), thy) = thy
       |> fold_map define_finite_const (dom_binds ~~ take_consts ~~ dom_eqns)