src/HOL/Nominal/nominal_atoms.ML
changeset 31781 861e675f01e6
parent 31737 b3f63611784e
child 31783 cfbe9609ceb1
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 23 12:09:30 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 23 14:50:34 2009 +0200
     1.3 @@ -101,7 +101,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 ({inject,case_thms,...},thy1) = Datatype.add_datatype
     1.8 +              val ((dt_names, {inject,case_thms,...}),thy1) = Datatype.add_datatype
     1.9                  Datatype.default_config [ak] [dt] thy
    1.10                val inject_flat = flat inject
    1.11                val ak_type = Type (Sign.intern_type thy1 ak,[])