1.1 --- a/src/HOL/Import/import_rule.ML	Fri Oct 12 18:58:20 2012 +0200
     1.2 +++ b/src/HOL/Import/import_rule.ML	Fri Oct 12 21:22:35 2012 +0200
     1.3 @@ -220,9 +220,8 @@
     1.4      val tfrees = Term.add_tfrees c []
     1.5      val tnames = sort_strings (map fst tfrees)
     1.6      val ((_, typedef_info), thy') =
     1.7 -     Typedef.add_typedef_global NONE
     1.8 -       (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
     1.9 -       (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy
    1.10 +     Typedef.add_typedef_global (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
    1.11 +       (SOME (Binding.name rep_name, Binding.name abs_name)) (rtac th2 1) thy
    1.12      val aty = #abs_type (#1 typedef_info)
    1.13      val th = freezeT (#type_definition (#2 typedef_info))
    1.14      val (th_s, _) = Thm.dest_comb (Thm.dest_arg (cprop_of th))