src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 33278 ba9f52f56356
parent 33173 b8ca12f6681a
child 33317 b4534348b8fd
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Oct 28 16:25:26 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Oct 28 16:25:27 2009 +0100
     1.3 @@ -153,13 +153,17 @@
     1.4          (descr' ~~ recTs ~~ rec_sets') ([], 0);
     1.5  
     1.6      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
     1.7 -        Inductive.add_inductive_global (serial ())
     1.8 +      thy0
     1.9 +      |> Sign.map_naming Name_Space.conceal
    1.10 +      |> Inductive.add_inductive_global (serial ())
    1.11            {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
    1.12              alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
    1.13              skip_mono = true, fork_mono = false}
    1.14            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    1.15            (map dest_Free rec_fns)
    1.16 -          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0;
    1.17 +          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
    1.18 +      ||> Sign.restore_naming thy0
    1.19 +      ||> Theory.checkpoint;
    1.20  
    1.21      (* prove uniqueness and termination of primrec combinators *)
    1.22