src/HOL/Tools/inductive_realizer.ML
changeset 52788 da1fdbfebd39
parent 51717 9e7d1c139569
child 54742 7a86358a3c0b
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jul 30 12:07:14 2013 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jul 30 15:09:25 2013 +0200
     1.3 @@ -298,7 +298,6 @@
     1.4        (map (fn (s, rs) => mk_realizes_eqn (not (member (op =) rsets s)) vs nparms rs) rss);
     1.5  
     1.6      val thy1' = thy1 |>
     1.7 -      Theory.copy |>
     1.8        Sign.add_types_global
     1.9          (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
    1.10        Extraction.add_typeof_eqns_i ty_eqs;