src/Pure/Isar/code.ML
changeset 58666 9e3426766267
parent 58665 50b229a5a097
child 59058 a78612c67ec0
equal deleted inserted replaced
58665:50b229a5a097 58666:9e3426766267
  1255     val constrs = map (unoverload_const_typ thy) proto_constrs;
  1255     val constrs = map (unoverload_const_typ thy) proto_constrs;
  1256     val (tyco, (vs, cos)) = constrset_of_consts thy constrs;
  1256     val (tyco, (vs, cos)) = constrset_of_consts thy constrs;
  1257   in
  1257   in
  1258     thy
  1258     thy
  1259     |> register_type (tyco, (vs, Constructors (cos, [])))
  1259     |> register_type (tyco, (vs, Constructors (cos, [])))
  1260     |> Named_Target.theory_map (Datatype_Plugin.data Plugin_Name.default_filter tyco)
  1260     |> Named_Target.theory_map (Datatype_Plugin.data_default tyco)
  1261   end;
  1261   end;
  1262 
  1262 
  1263 fun add_datatype_cmd raw_constrs thy =
  1263 fun add_datatype_cmd raw_constrs thy =
  1264   add_datatype (map (read_bare_const thy) raw_constrs) thy;
  1264   add_datatype (map (read_bare_const thy) raw_constrs) thy;
  1265 
  1265 
  1279   in
  1279   in
  1280     thy
  1280     thy
  1281     |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
  1281     |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
  1282     |> change_fun_spec rep
  1282     |> change_fun_spec rep
  1283       (K (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco)))
  1283       (K (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco)))
  1284     |> Named_Target.theory_map (Abstype_Plugin.data Plugin_Name.default_filter tyco)
  1284     |> Named_Target.theory_map (Abstype_Plugin.data_default tyco)
  1285   end;
  1285   end;
  1286 
  1286 
  1287 
  1287 
  1288 (* setup *)
  1288 (* setup *)
  1289 
  1289