src/HOL/Nominal/nominal_atoms.ML
changeset 45839 43a5b86bc102
parent 45701 615da8b8d758
child 45979 296d9a9c8d24
equal deleted inserted replaced
45838:653c84d5c6c9 45839:43a5b86bc102
    97 fun create_nom_typedecls ak_names thy =
    97 fun create_nom_typedecls ak_names thy =
    98   let
    98   let
    99     
    99     
   100     val (_,thy1) = 
   100     val (_,thy1) = 
   101     fold_map (fn ak => fn thy => 
   101     fold_map (fn ak => fn thy => 
   102           let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
   102           let val dt = ((Binding.name ak, [], NoSyn), [(Binding.name ak, [@{typ nat}], NoSyn)])
   103               val (dt_names, thy1) = Datatype.add_datatype Datatype.default_config [dt] thy;
   103               val (dt_names, thy1) = Datatype.add_datatype Datatype.default_config [dt] thy;
   104             
   104             
   105               val injects = maps (#inject o Datatype.the_info thy1) dt_names;
   105               val injects = maps (#inject o Datatype.the_info thy1) dt_names;
   106               val ak_type = Type (Sign.intern_type thy1 ak,[])
   106               val ak_type = Type (Sign.intern_type thy1 ak,[])
   107               val ak_sign = Sign.intern_const thy1 ak 
   107               val ak_sign = Sign.intern_const thy1 ak