src/HOL/Tools/inductive_realizer.ML

--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jul 30 12:07:14 2013 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jul 30 15:09:25 2013 +0200
@@ -298,7 +298,6 @@
       (map (fn (s, rs) => mk_realizes_eqn (not (member (op =) rsets s)) vs nparms rs) rss);
 
     val thy1' = thy1 |>
-      Theory.copy |>
       Sign.add_types_global
         (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
       Extraction.add_typeof_eqns_i ty_eqs;