src/HOL/Nominal/nominal_atoms.ML
changeset 45701 615da8b8d758
parent 45133 2214ba5bdfff
child 45839 43a5b86bc102
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Nov 30 21:14:01 2011 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Nov 30 23:30:08 2011 +0100
     1.3 @@ -100,8 +100,7 @@
     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, thy1) = Datatype.add_datatype
     1.8 -                Datatype.default_config [ak] [dt] thy;
     1.9 +              val (dt_names, thy1) = Datatype.add_datatype Datatype.default_config [dt] thy;
    1.10              
    1.11                val injects = maps (#inject o Datatype.the_info thy1) dt_names;
    1.12                val ak_type = Type (Sign.intern_type thy1 ak,[])