diff -r c143ad7811fc -r da1fdbfebd39 src/HOL/HOLCF/Tools/Domain/domain.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Tue Jul 30 12:07:14 2013 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Tue Jul 30 15:09:25 2013 +0200
@@ -68,7 +68,6 @@
 
     (* this theory is used just for parsing and error checking *)
     val tmp_thy = thy
-      |> Theory.copy
       |> fold (add_arity o thy_arity) dtnvs
 
     val dbinds : binding list =