src/HOLCF/Tools/Domain/domain_take_proofs.ML

     |> Sign.add_path path
     |> yield_singleton PureThy.add_thms
         (Thm.no_attributes (Binding.name name, thm))
     ||> Sign.parent_path;
 
+fun add_qualified_simp_thm name (path, thm) thy =
+    thy
+    |> Sign.add_path path
+    |> yield_singleton PureThy.add_thms
+        ((Binding.name name, thm), [Simplifier.simp_add])
+    ||> Sign.parent_path;
+
 (******************************************************************************)
 (************************** defining take functions ***************************)
 (******************************************************************************)
 
 fun define_take_functions

         val goal = mk_trp (mk_chain take_const);
         val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd};
         val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
         val thm = Goal.prove_global thy [] [] goal (K tac);
       in
-        thy
-          |> Sign.add_path dname
-          |> yield_singleton PureThy.add_thms
-              ((Binding.name "chain_take", thm), [Simplifier.simp_add])
-          ||> Sign.parent_path
+        add_qualified_simp_thm "chain_take" (dname, thm) thy
       end;
     val (chain_take_thms, thy) =
       fold_map prove_chain_take (take_consts ~~ dnames) thy;
 
     (* prove take_0 lemmas *)