src/HOL/Nominal/nominal_atoms.ML
changeset 27112 661a74bafeb7
parent 27095 c1c27955d7dd
child 27128 d2374ba6c02e
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 10 15:31:03 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 10 15:31:04 2008 +0200
     1.3 @@ -65,7 +65,7 @@
     1.4      val (_,thy1) = 
     1.5      fold_map (fn ak => fn thy => 
     1.6            let val dt = ([],ak,NoSyn,[(ak,[@{typ nat}],NoSyn)]) 
     1.7 -              val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype_i true false [ak] [dt] thy
     1.8 +              val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype true false [ak] [dt] thy
     1.9                val inject_flat = Library.flat inject
    1.10                val ak_type = Type (Sign.intern_type thy1 ak,[])
    1.11                val ak_sign = Sign.intern_const thy1 ak