src/HOL/Nominal/nominal_atoms.ML
changeset 31783 cfbe9609ceb1
parent 31781 861e675f01e6
child 31784 bd3486c57ba3
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 23 14:51:21 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 23 15:32:34 2009 +0200
     1.3 @@ -101,9 +101,10 @@
     1.4      val (_,thy1) = 
     1.5      fold_map (fn ak => fn thy => 
     1.6            let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
     1.7 -              val ((dt_names, {inject,case_thms,...}),thy1) = Datatype.add_datatype
     1.8 -                Datatype.default_config [ak] [dt] thy
     1.9 -              val inject_flat = flat inject
    1.10 +              val (dt_names, thy1) = Datatype.add_datatype
    1.11 +                Datatype.default_config [ak] [dt] thy;
    1.12 +            
    1.13 +              val injects = maps (#inject o Datatype.the_datatype thy1) dt_names;
    1.14                val ak_type = Type (Sign.intern_type thy1 ak,[])
    1.15                val ak_sign = Sign.intern_const thy1 ak 
    1.16                
    1.17 @@ -115,7 +116,7 @@
    1.18                    (Const (@{const_name "inj_on"},inj_on_type) $ 
    1.19                           Const (ak_sign,inj_type) $ HOLogic.mk_UNIV @{typ nat})
    1.20  
    1.21 -              val simp1 = @{thm inj_on_def}::inject_flat
    1.22 +              val simp1 = @{thm inj_on_def} :: injects;
    1.23                
    1.24                val proof1 = fn _ => EVERY [simp_tac (HOL_basic_ss addsimps simp1) 1,
    1.25                                            rtac @{thm ballI} 1,