--- a/src/HOL/Tools/inductive_realizer.ML Sun Apr 17 13:47:22 2011 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Sun Apr 17 19:54:04 2011 +0200
@@ -295,8 +295,9 @@
val thy1' = thy1 |>
Theory.copy |>
- Sign.add_types (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
- Extraction.add_typeof_eqns_i ty_eqs;
+ Sign.add_types_global
+ (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
+ Extraction.add_typeof_eqns_i ty_eqs;
val dts = map_filter (fn (s, rs) => if member (op =) rsets s then
SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;